toMatrixAlgEquiv_symm — Mathlib

English

For finite l and DecidableEq m, matrices A ∈ Mat_{l×m}(R) and B ∈ Mat_{m×n}(R) correspond to linear maps; their Lin-map composition equals the Lin-map of the product: Matrix.toLin v1 v3 (A B) = (Matrix.toLin v2 v3 A) ∘ (Matrix.toLin v1 v2 B).

Русский

Для A ∈ Mat_{l×m}(R) и B ∈ Mat_{m×n}(R) соответствующие линейные отображения удовлетворяют: Matrix.toLin v1 v3 (A B) = (Matrix.toLin v2 v3 A) ∘ (Matrix.toLin v1 v2 B).

LaTeX

$$$\mathrm{toLin}_{v_1,v_3}(A B) = \big( \mathrm{toLin}_{v_2,v_3}(A) \big) \circ \big( \mathrm{toLin}_{v_1,v_2}(B) \big)$$$

Lean4

@[simp]
theorem toMatrixAlgEquiv_symm : (LinearMap.toMatrixAlgEquiv v₁).symm = Matrix.toLinAlgEquiv v₁ :=
  rfl

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