[Merged by Bors] - refactor(data/polynomial/ring_division): Generalize irreducible_of_monic to no_zero_divisors

[tb65536]

This PR generalizes irreducible_of_monic to no_zero_divisors, using some of the work from @alreadydone's PR #17664.

Co-Authored-By: Junyan Xu junyanxumath@gmail.com

---

[Vierkantor]

LGTM, thanks! I went ahead and added a Co-Authored-By line in the PR description so Git is also aware of @alreadydone's contributions.

[Vierkantor]

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.

[alreadydone]

I think it's better to close this and merge my PR instead, otherwise there will be conflicts, since I didn't merge this PR into my PR.

[Vierkantor]

That's also fine for me if @tb65536 doesn't mind getting less credit in the Git statistics :)

[tb65536]

I think it's better to close this and merge my PR instead, otherwise there will be conflicts, since I didn't merge this PR into my PR.

@alreadydone I would still prefer to just go ahead and merge this, since it will make your PR more focused and easier to review. Yes, there will be some merge conflicts, but they should be easy to resolve since you already incorporated the changes. And then you can either use your results to further golf irreducible_of_monic or use irreducible_of_monic to golf your results.

[tb65536]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

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