matrix_eq_sum_single — Mathlib

English

A finite matrix x ∈ α^{m×n} can be written as the sum over all i ∈ m and j ∈ n of single i j (x_{i j}).

Русский

Конечную матрицу x ∈ α^{m×n} можно разложить как сумму по всем i ∈ m и j ∈ n: x = ∑_{i,j} single_{i j}(x_{i j}).

LaTeX

$$$ x = \sum_{i \in m} \sum_{j \in n} \mathrm{single}_{i j} (x_{i j}) $$$

Lean4

theorem matrix_eq_sum_single [AddCommMonoid α] [Fintype m] [Fintype n] (x : Matrix m n α) :
    x = ∑ i : m, ∑ j : n, single i j (x i j) := by
  ext i j
  rw [← Fintype.sum_prod_type']
  simp [single, Matrix.sum_apply, Matrix.of_apply, ← Prod.mk_inj]

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