algebraMap — Mathlib

English

The algebra map into matrices represents the corresponding algebra map on endomorphisms.

Русский

Алгебраическое отображение в матрицы представляет соответствующее отображение на эндоморфизмов.

LaTeX

$$Matrix.Represents.algebraMap r$$

Lean4

theorem algebraMap (r : R) : (algebraMap _ (Matrix ι ι R) r).Represents b (algebraMap _ (Module.End R M) r) := by
  simpa only [Algebra.algebraMap_eq_smul_one] using Matrix.Represents.one.smul r

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