Commit 2023-06-16 00:13 a3fde681

View on Github →

feat: port RingTheory.Polynomial.GaussLemma (#5069)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Polynomial/GaussLemma.lean

added theorem IsIntegrallyClosed.eq_map_mul_C_of_dvd

added theorem Polynomial.IsPrimitive.Int.dvd_iff_map_cast_dvd_map_cast

added theorem Polynomial.IsPrimitive.Int.irreducible_iff_irreducible_map_cast

added theorem Polynomial.IsPrimitive.dvd_iff_fraction_map_dvd_fraction_map

added theorem Polynomial.IsPrimitive.dvd_of_fraction_map_dvd_fraction_map

added theorem Polynomial.IsPrimitive.irreducible_iff_irreducible_map_fraction_map

added theorem Polynomial.IsPrimitive.irreducible_of_irreducible_map_of_injective

added theorem Polynomial.IsPrimitive.isUnit_iff_isUnit_map

added theorem Polynomial.IsPrimitive.isUnit_iff_isUnit_map_of_injective

added theorem Polynomial.Monic.dvd_iff_fraction_map_dvd_fraction_map

added theorem Polynomial.Monic.dvd_of_fraction_map_dvd_fraction_map

added theorem Polynomial.Monic.irreducible_iff_irreducible_map_fraction_map

added theorem Polynomial.isIntegrallyClosed_iff'

added theorem Polynomial.isUnit_or_eq_zero_of_isUnit_integerNormalization_primPart

added theorem integralClosure.mem_lifts_of_monic_of_dvd_map