[Merged by Bors] - feat(ring_theory/unique_factorization_domain): unique_factorization_monoid structure on polynomials over ufd

[awainverse]

Provides the unique_factorization_monoid structure on polynomials over a UFD

---

• depends on: feat(ring_theory/unique_factorization_domain): a normalization_monoid structure for ufms #4772

[jcommelin]

Wow, that was faster than I expected 🐙

[awainverse]

Does anyone know why this is causing class-instance depth problems, and how to avoid them?

[awainverse]

Fixed the major typo.

[hrmacbeth]

Can you please update docs/undergrad.yaml and docs/overview.yaml?

[awainverse]

I've added some entries to undergrad.yaml and overview.yaml.

[awainverse]

It seems #4772 merged a bit weirdly (@bryangingechen would understand...) so the diff probably appears larger than it really is?

[jcommelin]

@awainverse I'm nevertheless confused by the diff. Some of this stuff should now already be in mathlib, right?

[awainverse]

Yes, all the stuff from #4772 is already in mathlib, but still shows up as new changes in the diff.
@bryangingechen closed that PR, pointing out that "This was merged in 28cc74f".
Apparently this was the problem: bors-ng/bors-ng#1067
I'm still not sure how to update the diff here. I've already merged in master since the merge.

[bryangingechen]

I think I understand why the diff isn't correct. If I navigate to your most recent merge commit and then click on "View Diff", I get this page: 3f777ea

This shows that the two parents of that commit are 1f0ddac and e8f8de6. The former is the previous commit on this branch and the latter is indeed a commit from master; however, that commit does not include the commit corresponding to #4772 which is 28cc74f. If I browse the repo at that commit and look at the history, I see that e8f8de6 is 5 commits before 28cc74f.

In short, to get a good diff, you'll have to merge a commit from master which includes 28cc74f.

[awainverse]

Ok, I merged master again, and it worked. I'm not sure why my previous merge was too early.

[jcommelin]

Thanks 🎉

bors merge

[bors]

👎 Rejected by label

[bryangingechen]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

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