Commit 2023-06-03 19:30 5a5a09f6

View on Github →

feat: port Algebra.Lie.Abelian (#4631)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Lie/Abelian.lean

added theorem Function.Injective.isLieAbelian

added theorem Function.Surjective.isLieAbelian

added theorem LieAlgebra.abelian_of_le_center

added theorem LieAlgebra.ad_ker_eq_self_module_ker

added theorem LieAlgebra.isLieAbelian_bot

added theorem LieAlgebra.isLieAbelian_iff_center_eq_top

added theorem LieAlgebra.self_module_ker_eq_center

added theorem LieModule.coe_linearMap_maxTrivLinearMapEquivLieModuleHom

added theorem LieModule.coe_linearMap_maxTrivLinearMapEquivLieModuleHom_symm

added theorem LieModule.coe_maxTrivEquiv_apply

added theorem LieModule.coe_maxTrivHom_apply

added theorem LieModule.coe_maxTrivLinearMapEquivLieModuleHom

added theorem LieModule.coe_maxTrivLinearMapEquivLieModuleHom_symm

added theorem LieModule.ideal_oper_maxTrivSubmodule_eq_bot

added theorem LieModule.isTrivial_iff_max_triv_eq_top

added theorem LieModule.le_max_triv_iff_bracket_eq_bot

added def LieModule.maxTrivEquiv

added theorem LieModule.maxTrivEquiv_of_equiv_symm_eq_symm

added theorem LieModule.maxTrivEquiv_of_refl_eq_refl

added def LieModule.maxTrivHom

added def LieModule.maxTrivLinearMapEquivLieModuleHom

added def LieModule.maxTrivSubmodule

added theorem LieModule.mem_maxTrivSubmodule

added theorem LieModule.trivial_iff_le_maximal_trivial

added theorem LieSubmodule.lie_abelian_iff_lie_self_eq_bot

added theorem LieSubmodule.trivial_lie_oper_zero

added theorem commutative_ring_iff_abelian_lie_ring

added theorem lie_abelian_iff_equiv_lie_abelian

added theorem trivial_lie_zero