lieEquivMatrix'_apply — Mathlib

English

The Lie algebra equivalence sends an endomorphism f to its matrix representation: lieEquivMatrix' f = LinearMap.toMatrix' f.

Русский

Тождественный переход Ли‑алгебры переводит отображение f в его матричную запись: lieEquivMatrix' f = LinearMap.toMatrix' f.

LaTeX

$$$\\text{lieEquivMatrix'}(f) = \\text{LinearMap.toMatrix'}(f).$$$

Lean4

@[simp]
theorem lieEquivMatrix'_apply (f : Module.End R (n → R)) : lieEquivMatrix' f = LinearMap.toMatrix' f :=
  rfl

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