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 • Matrix.vecCons y v = Matrix.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 → α) : Matrix.vecCons x v + w = Matrix.vecCons (x + Matrix.vecHead w) (v + Matrix.vecTail w)

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

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)

@[simp]

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

@[simp]

theorem Matrix.tail_add {α : Type u_1} {n : ℕ} [Add α] (a b : Fin n.succ → α) : Matrix.vecTail (a + b) = Matrix.vecTail a + Matrix.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 → α) : Matrix.vecCons x v - w = Matrix.vecCons (x - Matrix.vecHead w) (v - Matrix.vecTail w)

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

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)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

theorem Matrix.cons_nonzero_iff {α : Type u_1} {n : ℕ} [Zero α] {v : Fin n → α} {x : α} : Matrix.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 → α) : -Matrix.vecCons x v = Matrix.vecCons (-x) (-v)

@[simp]

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

@[simp]

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