maxTrivEquiv_of_refl_eq_refl — Mathlib

English

The maximal trivial equivalence of the identity LieModuleEquiv is the identity equivalence.

Русский

Максимальная тривиальная эквивалентность для тождественного Ли-модуля равна тождественной эквивалентности.

LaTeX

$$$\\text{maxTrivEquiv}(\\mathrm{refl}) = \\mathrm{refl}$$$

Lean4

@[simp]
theorem maxTrivEquiv_of_refl_eq_refl : maxTrivEquiv (LieModuleEquiv.refl : M ≃ₗ⁅R,L⁆ M) = LieModuleEquiv.refl := by ext;
  simp only [coe_maxTrivEquiv_apply, LieModuleEquiv.refl_apply]

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