Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-20 07:56 0c721d5d

View on Github →

feat(algebra/lie/abelian): expand API for lie_module.maximal_trivial_submodule (#7235)

Estimated changes

Modified src/algebra/lie/abelian.lean

added theorem lie_module.coe_maximal_trivial_equiv_apply

added theorem lie_module.coe_maximal_trivial_hom_apply

added theorem lie_module.coe_maximal_trivial_linear_map_equiv_lie_module_hom_apply

added theorem lie_module.coe_maximal_trivial_linear_map_equiv_lie_module_hom_symm_apply

added def lie_module.maximal_trivial_equiv

added theorem lie_module.maximal_trivial_equiv_of_equiv_symm_eq_symm

added theorem lie_module.maximal_trivial_equiv_of_refl_eq_refl

added def lie_module.maximal_trivial_hom

added def lie_module.maximal_trivial_linear_map_equiv_lie_module_hom

Modified src/algebra/lie/basic.lean

added theorem lie_module_equiv.ext

added theorem lie_module_equiv.to_equiv_injective

modified structure lie_module_equiv