Commit 2023-01-14 15:15 7a030ab8

View on Github →

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

Estimated changes

Modified src/data/polynomial/splits.lean

added theorem polynomial.mem_lift_of_splits_of_roots_mem_range

Modified src/ring_theory/integral_closure.lean

added theorem roots_mem_integral_closure

Modified src/ring_theory/integrally_closed.lean

added theorem integral_closure.mem_lifts_of_monic_of_dvd_map

added theorem is_integrally_closed.eq_map_mul_C_of_dvd

Modified src/ring_theory/polynomial/content.lean

deleted theorem polynomial.is_primitive.is_primitive_of_dvd

added theorem polynomial.is_primitive_of_dvd

Modified src/ring_theory/polynomial/cyclotomic/basic.lean

Modified src/ring_theory/polynomial/gauss_lemma.lean

added theorem polynomial.is_integrally_closed_iff'

added theorem polynomial.monic.irreducible_iff_irreducible_map_fraction_map