Algebraic properties of tuples

@[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

@[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

@[simp]

theorem Fin.insertNth_mul {n : ℕ} {α : Fin (n + 1) → Type u_1} [(j : Fin (n + 1)) → Mul (α j)] (i : Fin (n + 1)) (x y : α i) (p q : (j : Fin n) → α (i.succAbove j)) : i.insertNth (x * y) (p * q) = i.insertNth x p * i.insertNth y q

@[simp]

theorem Fin.insertNth_add {n : ℕ} {α : Fin (n + 1) → Type u_1} [(j : Fin (n + 1)) → Add (α j)] (i : Fin (n + 1)) (x y : α i) (p q : (j : Fin n) → α (i.succAbove j)) : i.insertNth (x + y) (p + q) = i.insertNth x p + i.insertNth y q

@[simp]

theorem Fin.insertNth_div {n : ℕ} {α : Fin (n + 1) → Type u_1} [(j : Fin (n + 1)) → Div (α j)] (i : Fin (n + 1)) (x y : α i) (p q : (j : Fin n) → α (i.succAbove j)) : i.insertNth (x / y) (p / q) = i.insertNth x p / i.insertNth y q

@[simp]

theorem Fin.insertNth_sub {n : ℕ} {α : Fin (n + 1) → Type u_1} [(j : Fin (n + 1)) → Sub (α j)] (i : Fin (n + 1)) (x y : α i) (p q : (j : Fin n) → α (i.succAbove j)) : i.insertNth (x - y) (p - q) = i.insertNth x p - i.insertNth y q

@[simp]

theorem Fin.insertNth_div_same {n : ℕ} {α : Fin (n + 1) → Type u_1} [(j : Fin (n + 1)) → Group (α j)] (i : Fin (n + 1)) (x y : α i) (p : (j : Fin n) → α (i.succAbove j)) : i.insertNth x p / i.insertNth y p = Pi.mulSingle i (x / y)

@[simp]

theorem Fin.insertNth_sub_same {n : ℕ} {α : Fin (n + 1) → Type u_1} [(j : Fin (n + 1)) → AddGroup (α j)] (i : Fin (n + 1)) (x y : α i) (p : (j : Fin n) → α (i.succAbove j)) : i.insertNth x p - i.insertNth y p = Pi.single i (x - y)

@[simp]

theorem Matrix.smul_empty {α : Type u_1} {M : Type u_2} [SMul M α] (x : M) (v : Fin 0 → α) : x • v = ![]

@[simp]

theorem Matrix.smul_cons {α : Type u_1} {M : Type u_2} {n : ℕ} [SMul M α] (x : M) (y : α) (v : Fin n → α) : x • vecCons y v = vecCons (x • y) (x • v)

@[simp]

theorem Matrix.empty_add_empty {α : Type u_1} [Add α] (v w : Fin 0 → α) : v + w = ![]

@[simp]

theorem Matrix.cons_add {α : Type u_1} {n : ℕ} [Add α] (x : α) (v : Fin n → α) (w : Fin n.succ → α) : vecCons x v + w = vecCons (x + vecHead w) (v + vecTail w)

@[simp]

theorem Matrix.add_cons {α : Type u_1} {n : ℕ} [Add α] (v : Fin n.succ → α) (y : α) (w : Fin n → α) : v + vecCons y w = vecCons (vecHead v + y) (vecTail v + w)

theorem Matrix.cons_add_cons {α : Type u_1} {n : ℕ} [Add α] (x : α) (v : Fin n → α) (y : α) (w : Fin n → α) : vecCons x v + vecCons y w = vecCons (x + y) (v + w)

@[simp]

theorem Matrix.head_add {α : Type u_1} {n : ℕ} [Add α] (a b : Fin n.succ → α) : vecHead (a + b) = vecHead a + vecHead b

@[simp]

theorem Matrix.tail_add {α : Type u_1} {n : ℕ} [Add α] (a b : Fin n.succ → α) : vecTail (a + b) = vecTail a + vecTail b

@[simp]

theorem Matrix.empty_sub_empty {α : Type u_1} [Sub α] (v w : Fin 0 → α) : v - w = ![]

@[simp]

theorem Matrix.cons_sub {α : Type u_1} {n : ℕ} [Sub α] (x : α) (v : Fin n → α) (w : Fin n.succ → α) : vecCons x v - w = vecCons (x - vecHead w) (v - vecTail w)

@[simp]

theorem Matrix.sub_cons {α : Type u_1} {n : ℕ} [Sub α] (v : Fin n.succ → α) (y : α) (w : Fin n → α) : v - vecCons y w = vecCons (vecHead v - y) (vecTail v - w)

theorem Matrix.cons_sub_cons {α : Type u_1} {n : ℕ} [Sub α] (x : α) (v : Fin n → α) (y : α) (w : Fin n → α) : vecCons x v - vecCons y w = vecCons (x - y) (v - w)

@[simp]

theorem Matrix.head_sub {α : Type u_1} {n : ℕ} [Sub α] (a b : Fin n.succ → α) : vecHead (a - b) = vecHead a - vecHead b

@[simp]

theorem Matrix.tail_sub {α : Type u_1} {n : ℕ} [Sub α] (a b : Fin n.succ → α) : vecTail (a - b) = vecTail a - vecTail b

@[simp]

theorem Matrix.zero_empty {α : Type u_1} [Zero α] : 0 = ![]

@[simp]

theorem Matrix.cons_zero_zero {α : Type u_1} {n : ℕ} [Zero α] : vecCons 0 0 = 0

@[simp]

theorem Matrix.head_zero {α : Type u_1} {n : ℕ} [Zero α] : vecHead 0 = 0

@[simp]

theorem Matrix.tail_zero {α : Type u_1} {n : ℕ} [Zero α] : vecTail 0 = 0

@[simp]

theorem Matrix.cons_eq_zero_iff {α : Type u_1} {n : ℕ} [Zero α] {v : Fin n → α} {x : α} : vecCons x v = 0 ↔ x = 0 ∧ v = 0

theorem Matrix.cons_nonzero_iff {α : Type u_1} {n : ℕ} [Zero α] {v : Fin n → α} {x : α} : vecCons x v ≠ 0 ↔ x ≠ 0 ∨ v ≠ 0

@[simp]

theorem Matrix.neg_empty {α : Type u_1} [Neg α] (v : Fin 0 → α) : -v = ![]

@[simp]

theorem Matrix.neg_cons {α : Type u_1} {n : ℕ} [Neg α] (x : α) (v : Fin n → α) : -vecCons x v = vecCons (-x) (-v)

@[simp]

theorem Matrix.head_neg {α : Type u_1} {n : ℕ} [Neg α] (a : Fin n.succ → α) : vecHead (-a) = -vecHead a

@[simp]

theorem Matrix.tail_neg {α : Type u_1} {n : ℕ} [Neg α] (a : Fin n.succ → α) : vecTail (-a) = -vecTail a