[Merged by Bors] - feat(algebra/lie/nilpotent): a non-trivial nilpotent Lie module has non-trivial maximal trivial submodule

[ocfnash]

The main result is lie_module.nontrivial_max_triv_of_is_nilpotent

---

[jcommelin]

One slight concern is that nilpotency_length and lower_central_series_last are both fairly long names for a definition. But maybe they will not be used too much, so it's fine.
Of course we can easily refactor later.

[ocfnash]

One slight concern is that nilpotency_length and lower_central_series_last are both fairly long names for a definition. But maybe they will not be used too much, so it's fine. Of course we can easily refactor later.

I share the concern but have persuaded myself these are OK for the reasons you state.

I'm happy to rename / wait for inspiration though. Right now, I can think of the following alternatives for nilpotency_length:

• nilpotency_len
• lcs_length
• lcs_len

and the following for lower_central_series_last just lcs_last.

[jcommelin]

Oops, I forgot a comma,

bors d+

[bors]

✌️ ocfnash can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[jcommelin]

Let's leave the names as is. We can refactor later. Maybe lower_central_series should just become lcs like you suggest. It has been bumping name lengths in other part of Lie theory as well. But we should then do the same in group theory.

[ocfnash]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests