toMatrix'_algebraMap — Mathlib

English

If M and M' are mutual inverses, then the linear map defined by M' is an isomorphism with inverse given by the map defined by M.

Русский

Если M и M' взаимно обратны, то линейное отображение, задаваемое M', является изоморфизмом с обратным отображением через M.

LaTeX

$$$ \\text{If } M M' = I_m \\text{ and } M' M = I_n, \\text{ then } \\mathrm{toLin'}(M') \\text{ is a linear equivalence with inverse } \\mathrm{toLin'}(M). $$$

Lean4

@[simp]
theorem toMatrix'_algebraMap (x : R) : LinearMap.toMatrix' (algebraMap R (Module.End R (n → R)) x) = scalar n x := by
  simp [Module.algebraMap_end_eq_smul_id, smul_eq_diagonal_mul]

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