Commit 2021-01-06 08:30 648ff216

View on Github →

feat(algebra/lie/basic): the lattice of Lie submodules of a Noetherian Lie module is well-founded (#5557) The key result is: well_founded_of_noetherian

Estimated changes

Modified src/algebra/lie/basic.lean

added theorem lie_submodule.coe_submodule_injective

added theorem lie_submodule.mem_coe_submodule

added theorem lie_submodule.well_founded_of_noetherian