basic): the lattice of Lie submodules of a Noetherian Lie module is well-founded (#5557)

Commit

5 years ago

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`

Author

Oliver Nash

Parents

38921554

mathlib 648ff216 - feat(algebra/lie/basic): the lattice of Lie submodules of a Noetherian Lie module is well-founded (#5557)

mathlib
648ff216 - feat(algebra/lie/basic): the lattice of Lie submodules of a Noetherian Lie module is well-founded (#5557)