HepLean Documentation

Mathlib.Algebra.Group.Fin.Tuple

Algebraic properties of tuples #

source
@[simp]
theorem Fin.insertNth_zero_right {n : ℕ} {α : Fin (n + 1) → Type u_1} [(j : Fin (n + 1)) → Zero (α j)] (i : Fin (n + 1)) (x : α i) :
i.insertNth x 0 = Pi.single i x
source
@[simp]
theorem Fin.insertNth_one_right {n : ℕ} {α : Fin (n + 1) → Type u_1} [(j : Fin (n + 1)) → One (α j)] (i : Fin (n + 1)) (x : α i) :
i.insertNth x 1 = Pi.mulSingle i x
source
@[simp]
theorem Fin.insertNth_add {n : ℕ} {α : Fin (n + 1) → Type u_1} [(j : Fin (n + 1)) → Add (α j)] (i : Fin (n + 1)) (x : α i) (y : α i) (p : (j : Fin n) → α (i.succAbove j)) (q : (j : Fin n) → α (i.succAbove j)) :
i.insertNth (x + y) (p + q) = i.insertNth x p + i.insertNth y q
source
@[simp]
theorem Fin.insertNth_mul {n : ℕ} {α : Fin (n + 1) → Type u_1} [(j : Fin (n + 1)) → Mul (α j)] (i : Fin (n + 1)) (x : α i) (y : α i) (p : (j : Fin n) → α (i.succAbove j)) (q : (j : Fin n) → α (i.succAbove j)) :
i.insertNth (x * y) (p * q) = i.insertNth x p * i.insertNth y q
source
@[simp]
theorem Fin.insertNth_sub {n : ℕ} {α : Fin (n + 1) → Type u_1} [(j : Fin (n + 1)) → Sub (α j)] (i : Fin (n + 1)) (x : α i) (y : α i) (p : (j : Fin n) → α (i.succAbove j)) (q : (j : Fin n) → α (i.succAbove j)) :
i.insertNth (x - y) (p - q) = i.insertNth x p - i.insertNth y q
source
@[simp]
theorem Fin.insertNth_div {n : ℕ} {α : Fin (n + 1) → Type u_1} [(j : Fin (n + 1)) → Div (α j)] (i : Fin (n + 1)) (x : α i) (y : α i) (p : (j : Fin n) → α (i.succAbove j)) (q : (j : Fin n) → α (i.succAbove j)) :
i.insertNth (x / y) (p / q) = i.insertNth x p / i.insertNth y q
source
@[simp]
theorem Fin.insertNth_sub_same {n : ℕ} {α : Fin (n + 1) → Type u_1} [(j : Fin (n + 1)) → AddGroup (α j)] (i : Fin (n + 1)) (x : α i) (y : α i) (p : (j : Fin n) → α (i.succAbove j)) :
i.insertNth x p - i.insertNth y p = Pi.single i (x - y)
source
@[simp]
theorem Fin.insertNth_div_same {n : ℕ} {α : Fin (n + 1) → Type u_1} [(j : Fin (n + 1)) → Group (α j)] (i : Fin (n + 1)) (x : α i) (y : α i) (p : (j : Fin n) → α (i.succAbove j)) :
i.insertNth x p / i.insertNth y p = Pi.mulSingle i (x / y)
source
@[simp]
theorem Matrix.smul_empty {α : Type u_1} {M : Type u_2} [SMul M α] (x : M) (v : Fin 0 → α) :
x • v = ![]
source
@[simp]
theorem Matrix.smul_cons {α : Type u_1} {M : Type u_2} {n : ℕ} [SMul M α] (x : M) (y : α) (v : Fin n → α) :
x • Matrix.vecCons y v = Matrix.vecCons (x • y) (x • v)
source
@[simp]
theorem Matrix.empty_add_empty {α : Type u_1} [Add α] (v : Fin 0 → α) (w : Fin 0 → α) :
v + w = ![]
source
@[simp]
theorem Matrix.cons_add {α : Type u_1} {n : ℕ} [Add α] (x : α) (v : Fin n → α) (w : Fin n.succ → α) :
Matrix.vecCons x v + w = Matrix.vecCons (x + Matrix.vecHead w) (v + Matrix.vecTail w)
source
@[simp]
theorem Matrix.add_cons {α : Type u_1} {n : ℕ} [Add α] (v : Fin n.succ → α) (y : α) (w : Fin n → α) :
v + Matrix.vecCons y w = Matrix.vecCons (Matrix.vecHead v + y) (Matrix.vecTail v + w)
source
theorem Matrix.cons_add_cons {α : Type u_1} {n : ℕ} [Add α] (x : α) (v : Fin n → α) (y : α) (w : Fin n → α) :
Matrix.vecCons x v + Matrix.vecCons y w = Matrix.vecCons (x + y) (v + w)
source
@[simp]
theorem Matrix.head_add {α : Type u_1} {n : ℕ} [Add α] (a : Fin n.succ → α) (b : Fin n.succ → α) :
Matrix.vecHead (a + b) = Matrix.vecHead a + Matrix.vecHead b
source
@[simp]
theorem Matrix.tail_add {α : Type u_1} {n : ℕ} [Add α] (a : Fin n.succ → α) (b : Fin n.succ → α) :
Matrix.vecTail (a + b) = Matrix.vecTail a + Matrix.vecTail b
source
@[simp]
theorem Matrix.empty_sub_empty {α : Type u_1} [Sub α] (v : Fin 0 → α) (w : Fin 0 → α) :
v - w = ![]
source
@[simp]
theorem Matrix.cons_sub {α : Type u_1} {n : ℕ} [Sub α] (x : α) (v : Fin n → α) (w : Fin n.succ → α) :
Matrix.vecCons x v - w = Matrix.vecCons (x - Matrix.vecHead w) (v - Matrix.vecTail w)
source
@[simp]
theorem Matrix.sub_cons {α : Type u_1} {n : ℕ} [Sub α] (v : Fin n.succ → α) (y : α) (w : Fin n → α) :
v - Matrix.vecCons y w = Matrix.vecCons (Matrix.vecHead v - y) (Matrix.vecTail v - w)
source
theorem Matrix.cons_sub_cons {α : Type u_1} {n : ℕ} [Sub α] (x : α) (v : Fin n → α) (y : α) (w : Fin n → α) :
Matrix.vecCons x v - Matrix.vecCons y w = Matrix.vecCons (x - y) (v - w)
source
@[simp]
theorem Matrix.head_sub {α : Type u_1} {n : ℕ} [Sub α] (a : Fin n.succ → α) (b : Fin n.succ → α) :
Matrix.vecHead (a - b) = Matrix.vecHead a - Matrix.vecHead b
source
@[simp]
theorem Matrix.tail_sub {α : Type u_1} {n : ℕ} [Sub α] (a : Fin n.succ → α) (b : Fin n.succ → α) :
Matrix.vecTail (a - b) = Matrix.vecTail a - Matrix.vecTail b
source
@[simp]
theorem Matrix.zero_empty {α : Type u_1} [Zero α] :
0 = ![]
source
@[simp]
theorem Matrix.cons_zero_zero {α : Type u_1} {n : ℕ} [Zero α] :
Matrix.vecCons 0 0 = 0
source
@[simp]
theorem Matrix.head_zero {α : Type u_1} {n : ℕ} [Zero α] :
Matrix.vecHead 0 = 0
source
@[simp]
theorem Matrix.tail_zero {α : Type u_1} {n : ℕ} [Zero α] :
Matrix.vecTail 0 = 0
source
@[simp]
theorem Matrix.cons_eq_zero_iff {α : Type u_1} {n : ℕ} [Zero α] {v : Fin n → α} {x : α} :
Matrix.vecCons x v = 0 ↔ x = 0 ∧ v = 0
source
theorem Matrix.cons_nonzero_iff {α : Type u_1} {n : ℕ} [Zero α] {v : Fin n → α} {x : α} :
Matrix.vecCons x v ≠ 0 ↔ x ≠ 0 ∨ v ≠ 0
source
@[simp]
theorem Matrix.neg_empty {α : Type u_1} [Neg α] (v : Fin 0 → α) :
-v = ![]
source
@[simp]
theorem Matrix.neg_cons {α : Type u_1} {n : ℕ} [Neg α] (x : α) (v : Fin n → α) :
-Matrix.vecCons x v = Matrix.vecCons (-x) (-v)
source
@[simp]
theorem Matrix.head_neg {α : Type u_1} {n : ℕ} [Neg α] (a : Fin n.succ → α) :
Matrix.vecHead (-a) = -Matrix.vecHead a
source
@[simp]
theorem Matrix.tail_neg {α : Type u_1} {n : ℕ} [Neg α] (a : Fin n.succ → α) :
Matrix.vecTail (-a) = -Matrix.vecTail a