[Merged by Bors] - feat: define the positive Fitting component of the representation of a nilpotent Lie algebra

[ocfnash]

---

• depends on: [Merged by Bors] - feat: lemmas about divisibility, mostly related to nilpotency #7355

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• [Merged by Bors] - feat: lemmas about divisibility, mostly related to nilpotency #7355
  By Dependent Issues (🤖). Happy coding!

[kbuzzard]

This looks great to me. I couldn't find anything to say about the code. If some of this stuff is original research or hard to find in the literature, do you think it's worth mentioning somewhere?

[ocfnash]

This looks great to me. I couldn't find anything to say about the code. If some of this stuff is original research or hard to find in the literature, do you think it's worth mentioning somewhere?

Repeating what I wrote in a now-hidden comment above: I think a small module doc string explanation may be merited when I add the proof of IsCompl (weightSpace M 0) (posFittingComp R L M) (which I have locally but depends on five open PRs).

[kbuzzard]

Thanks!

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by kbuzzard.

[jcommelin]

Thanks 🎉

bors merge

[bors]

Build failed:

• Build

[ocfnash]

The build failure was due to a "No space left on device" error for hoskinson9, so I'll try sending this back to bors in the hopes of getting a different runner.

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style