Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-11 16:21 abf72e6d

View on Github →

refactor(algebra/lie/*): rename lie_algebra.morphism --> lie_hom, lie_algebra.equiv --> lie_equiv (#6179) Also renaming the field map_lie to map_lie' in both lie_algebra.morphism and lie_module_hom for consistency with the pattern elsewhere in Mathlib.

Estimated changes

deleted theorem lie_algebra.coe_mk
deleted structure lie_algebra.equiv
deleted theorem lie_algebra.map_lie
deleted theorem lie_algebra.map_zero
deleted theorem lie_algebra.morphism.ext
deleted structure lie_algebra.morphism
added theorem lie_equiv.bijective
added theorem lie_equiv.injective
added theorem lie_equiv.one_apply
added def lie_equiv.refl
added theorem lie_equiv.refl_apply
added theorem lie_equiv.surjective
added def lie_equiv.symm
added theorem lie_equiv.symm_symm
added def lie_equiv.trans
added theorem lie_equiv.trans_apply
added structure lie_equiv
added theorem lie_hom.coe_injective
added theorem lie_hom.coe_mk
added def lie_hom.comp
added theorem lie_hom.comp_apply
added theorem lie_hom.comp_coe
added theorem lie_hom.ext
added theorem lie_hom.ext_iff
added def lie_hom.inverse
added theorem lie_hom.map_add
added theorem lie_hom.map_lie
added theorem lie_hom.map_smul
added theorem lie_hom.map_zero
added structure lie_hom
deleted theorem lie_module_hom.map_lie'
added theorem lie_module_hom.map_lie
added def lie_equiv.of_eq
added theorem lie_equiv.of_eq_apply
added def lie_hom.range
added theorem lie_hom.range_bracket
added theorem lie_hom.range_coe
added def lie_hom.ker
added theorem lie_hom.ker_eq_bot
added theorem lie_hom.ker_le_comap
added theorem lie_hom.le_ker_iff
added theorem lie_hom.map_bot_iff
added theorem lie_hom.mem_ker