Commit 2021-06-28 12:36 f7c1e5f2

View on Github →

feat(algebra/lie/nilpotent): basic lemmas about nilpotency for Lie subalgebras of associative algebras (#8090) The main lemma is: lie_algebra.is_nilpotent_ad_of_is_nilpotent which is the first step in proving Engel's theorem.

Estimated changes

Modified src/algebra/algebra/basic.lean

added theorem algebra.commute_lmul_left_right

added theorem algebra.lmul_left_eq_zero_iff

added theorem algebra.lmul_left_zero_eq_zero

added theorem algebra.lmul_right_eq_zero_iff

added theorem algebra.lmul_right_zero_eq_zero

added theorem algebra.pow_lmul_left

added theorem algebra.pow_lmul_right

Modified src/algebra/lie/nilpotent.lean

added theorem lie_algebra.ad_nilpotent_of_nilpotent

added theorem lie_algebra.is_nilpotent_ad_of_is_nilpotent

added theorem lie_subalgebra.is_nilpotent_ad_of_is_nilpotent_ad

Modified src/algebra/lie/of_associative.lean

added theorem lie_algebra.ad_eq_lmul_left_sub_lmul_right

added theorem lie_subalgebra.ad_comp_incl_eq

Modified src/linear_algebra/basic.lean

added theorem linear_map.submodule_pow_eq_zero_of_pow_eq_zero

Modified src/ring_theory/nilpotent.lean

added theorem algebra.is_nilpotent_lmul_left_iff

added theorem algebra.is_nilpotent_lmul_right_iff