[Merged by Bors] - feat(data/polynomial/unit_trinomial): Irreducibility of X^n-X-1

[tb65536]

This PR adds a proves irreducibility of X^n-X-1, superseding #6421.

---

[riccardobrasca]

There is a reason why this is in data? It contains a nontrivial theorem, I have the impression it is better to have it in ring_theory.polynomial

[tb65536]

There is a reason why this is in data? It contains a nontrivial theorem, I have the impression it is better to have it in ring_theory.polynomial

Ah, I'll move this file to ring_theory.polynomial then. I was just putting the polynomial in the same folder as mirror.lean and reverse.lean.

[riccardobrasca]

There is a reason why this is in data? It contains a nontrivial theorem, I have the impression it is better to have it in ring_theory.polynomial

Ah, I'll move this file to ring_theory.polynomial then. I was just putting the polynomial in the same folder as mirror.lean and reverse.lean.

You can keep the definiton and the basic API in data, but the theorems are usually elsewhere.

[riccardobrasca]

Thanks!

bors d+

[bors]

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

[tb65536]

bors r+

[bors]

This PR was included in a batch that was canceled, it will be automatically retried

[bors]

Pull request successfully merged into master.

Build succeeded:

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