mathlib3

7a030ab8 - feat(ring_theory/polynomial/gauss_lemma): Prove Gauss's Lemma for integrally closed rings (#18147)

feat(ring_theory/polynomial/gauss_lemma): Prove Gauss's Lemma for integrally closed rings (#18147) In this PR, we prove Gauss's lemma for integrally closed rings. See #18021 and #11523 for previous discussion on the topic. We also show that integrally closed domains are precisely the domains in which Gauss's lemma holds for monic polynomials. [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2318021.20generalizing.20theory.20of.20minpoly) Co-authored-by: Junyan Xu <junyanxu.math@gmail.com> Co-authored-by: Paul Lezeau <paul.lezeau@gmail.com>