Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-22 20:22 a1f3ff85

View on Github →

feat(algebra/lie/nilpotent): basic lemmas about nilpotency (#7181)

Estimated changes

Modified src/algebra/lie/ideal_operations.lean

added theorem lie_submodule.lie_coe_mem_lie

modified theorem lie_submodule.lie_mem_lie

Modified src/algebra/lie/nilpotent.lean

added theorem lie_algebra.infi_max_gen_zero_eigenspace_eq_top_of_nilpotent

added theorem lie_algebra.nilpotent_ad_of_nilpotent_algebra

added theorem lie_module.infi_max_gen_zero_eigenspace_eq_top_of_nilpotent

added theorem lie_module.iterate_to_endomorphism_mem_lower_central_series

added theorem lie_module.nilpotent_endo_of_nilpotent_module

Modified src/linear_algebra/basic.lean

modified theorem submodule.coe_scott_continuous