single_add — Mathlib

English

For an additive type α, the single matrix is additive in its entry: single i j (a + b) = single i j a + single i j b.

Русский

Для аддитивного типа α элемент-матрица имеет линейность по значению: single i j (a + b) = single i j a + single i j b.

LaTeX

$$$ \mathrm{single}_{i j} (a + b) = \mathrm{single}_{i j} a + \mathrm{single}_{i j} b $$$

Lean4

theorem single_add [AddZeroClass α] (i : m) (j : n) (a b : α) : single i j (a + b) = single i j a + single i j b :=
  by
  ext
  simp only [single, of_apply]
  split_ifs with h <;> simp [h]

Похожие утверждения