Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-18 12:22 5bbc187e

View on Github →

feat(algebra/lie/nilpotent): a non-trivial nilpotent Lie module has non-trivial maximal trivial submodule (#11515) The main result is lie_module.nontrivial_max_triv_of_is_nilpotent

Estimated changes

Modified src/algebra/lie/abelian.lean

added theorem lie_module.le_max_triv_iff_bracket_eq_bot

Modified src/algebra/lie/ideal_operations.lean

added theorem lie_submodule.lie_eq_bot_iff

Modified src/algebra/lie/nilpotent.lean

added theorem lie_module.antitone_lower_central_series

added theorem lie_module.lower_central_series_last_le_max_triv

added theorem lie_module.nilpotency_length_eq_succ_iff

added theorem lie_module.nilpotency_length_eq_zero_iff

added theorem lie_module.nontrivial_lower_central_series_last

added theorem lie_module.nontrivial_max_triv_of_is_nilpotent

Modified src/algebra/lie/submodule.lean

added theorem lie_submodule.lie_span_eq_bot_iff

added theorem lie_submodule.nontrivial_iff_ne_bot

Modified src/data/set/basic.lean

added theorem set.nontrivial_mono