matrix_components — Mathlib

English

For any matrix m of morphisms m_{j k}: f(j) → g(k), the (j,k)-entry of the matrix obtained from m by biproduct.matrix equals m_{j k}.

Русский

Для любой матрицы морфизмов m_{j k}: f(j) → g(k) элемент (j,k) матрицы, полученной как biproduct.matrix m, равен m_{j k}.

LaTeX

$$$ \\operatorname{biproduct.components} ( \\operatorname{biproduct.matrix} m )\, j \, k = m\, j \, k $$$

Lean4

@[simp]
theorem matrix_components (m : ∀ j k, f j ⟶ g k) (j : J) (k : K) :
    biproduct.components (biproduct.matrix m) j k = m j k := by simp [biproduct.components]

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