[Merged by Bors] - feat(Algebra/Lie): Engel subalgebras

[jcommelin]

Progress toward #10065

---

[ocfnash]

Thanks, this is great.

Apart from the inline nitpicks, I wonder if we should take this as an opportunity to reorganise a few files. E.g., we could have a new LieSubalgebra folder containing:
Basic (current contents of LieSubalgebra.lean)
Cartan
Engel

bors d+

[mathlib-bors]

✌️ jcommelin 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]

Apart from the inline nitpicks, I wonder if we should take this as an opportunity to reorganise a few files. E.g., we could have a new LieSubalgebra folder containing: Basic (current contents of LieSubalgebra.lean) Cartan Engel

Sounds good. We can do that in a follow-up as well.

[jcommelin]

bors merge

[mathlib-bors]

Build failed (retrying...):

• Build

[urkud]

Please run lake exe shake --fix
bors r-

[mathlib-bors]

Canceled.

[jcommelin]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style