symm — Mathlib

English

Lie module equivalences are symmetric: given an equivalence e: M ≃ₗ⁅R,L⁆ N, there exists a symmetric equivalence e.symm: N ≃ₗ⁅R,L⁆ M.

Русский

Эквалентности модулей Ли симметричны: для эквалентности e: M ≃ₗ⁅R,L⁆ N существует симметричная эквалентность e.symm: N ≃ₗ⁅R,L⁆ M.

LaTeX

$$def symm (e : M ≃ₗ⁅R,L⁆ N) : N ≃ₗ⁅R,L⁆ M$$

Lean4

/-- Lie module equivalences are symmetric. -/
@[symm]
def symm (e : M ≃ₗ⁅R,L⁆ N) : N ≃ₗ⁅R,L⁆ M :=
  { LieModuleHom.inverse e.toLieModuleHom e.invFun e.left_inv e.right_inv, (e : M ≃ₗ[R] N).symm with }

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