Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-09 13:01 09afb046

View on Github →

feat(ring_theory/polynomial/content): Gauss's Lemma (irreducibility criterion) (#4861) Proves that a primitive polynomial is irreducible iff it is irreducible over the fraction field

Estimated changes

Modified src/data/polynomial/ring_division.lean

deleted theorem polynomial.irreducible_of_irreducible_map

added theorem polynomial.monic.irreducible_of_irreducible_map

Modified src/field_theory/algebraic_closure.lean

Modified src/ring_theory/localization.lean

Modified src/ring_theory/polynomial/content.lean

added theorem polynomial.is_primitive.is_primitive_of_dvd

Created src/ring_theory/polynomial/gauss_lemma.lean

added theorem polynomial.is_primitive.int.irreducible_iff_irreducible_map_cast

added theorem polynomial.is_primitive.irreducible_iff_irreducible_map_fraction_map

added theorem polynomial.is_primitive.irreducible_of_irreducible_map_of_injective

added theorem polynomial.is_primitive.is_unit_iff_is_unit_map

added theorem polynomial.is_primitive.is_unit_iff_is_unit_map_of_injective

added theorem polynomial.is_unit_or_eq_zero_of_is_unit_integer_normalization_prim_part