toLinearEquiv — Mathlib

English

There is a canonical linear equivalence associated to a Lie module equivalence, i.e., a structure-preserving linear isomorphism M ≃ N corresponding to e.

Русский

Существует каноническое линейное эквивалентное отображение, связанное с эквивалентностью модулей Ли, то есть линейное изоморфизм M ≃ N, соответствующий e.

LaTeX

$$$e: M \simeq_{\text{Lie}} N \quad\Rightarrow\quad M \cong_R N$$

Lean4

/-- View an equivalence of Lie modules as a linear equivalence. -/
def toLinearEquiv (e : M ≃ₗ⁅R,L⁆ N) : M ≃ₗ[R] N :=
  { e with }

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