algEquivMatrix' — Mathlib

English

The map e from M1 to M2 sends the product in End_S M1 to the corresponding product in End_S M2 via conjugation.

Русский

Отображение e переводит произведение в End_S M1 в соответствующее произведение в End_S M2 по конъюгации.

LaTeX

$$$\forall x,y\in \operatorname{End}_S M_1:\; e (x \cdot y) = e(x) \cdot e(y).$$$

Lean4

/-- The natural equivalence between linear endomorphisms of finite free modules and square matrices
is compatible with the algebra structures. -/
def algEquivMatrix' [Fintype n] : Module.End R (n → R) ≃ₐ[R] Matrix n n R :=
  LinearMap.toMatrixAlgEquiv'

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