Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-07 23:41 9411b00e

View on Github →

feat(algebra/lie/basic): define the center of a Lie algebra and prove some related results (#6013)

Estimated changes

Modified src/algebra/lie/basic.lean

added theorem lie_algebra.abelian_of_le_center

added theorem lie_algebra.abelian_radical_iff_solvable_is_abelian

added theorem lie_algebra.abelian_radical_of_semisimple

modified def lie_algebra.ad

added def lie_algebra.center

added theorem lie_algebra.center_eq_adjoint_kernel

added theorem lie_algebra.center_eq_bot_of_semisimple

added theorem lie_algebra.center_le_radical

added theorem lie_algebra.is_lie_abelian_iff_center_eq_top

deleted theorem lie_algebra.of_abelian_is_solvable

added theorem lie_algebra.subsingleton_of_semisimple_lie_abelian

deleted theorem lie_ideal.of_bot_eq_bot

added theorem lie_ideal.subsingleton_of_bot

deleted theorem lie_ideal.unique_of_bot

added theorem lie_module.is_trivial_iff_maximal_trivial_eq_top

added def lie_module.maximal_trivial_submodule

added theorem lie_module.mem_maximal_trivial_submodule

deleted def lie_module.to_endo_morphism

added def lie_module.to_endomorphism

added theorem lie_module.trivial_iff_le_maximal_trivial

deleted theorem lie_submodule.of_bot_eq_bot

added theorem lie_submodule.subsingleton_of_bot

deleted theorem lie_submodule.unique_of_bot