Commit 2022-11-24 15:26 86754809

View on Github →

refactor(data/polynomial/ring_division): Generalize irreducible_of_monic to no_zero_divisors (#17696) This PR generalizes irreducible_of_monic to no_zero_divisors, using some of the work from @alreadydone's PR #17664. Co-Authored-By: Junyan Xu junyanxumath@gmail.com

Estimated changes

Modified src/data/polynomial/coeff.lean

added theorem polynomial.is_unit_C

Modified src/data/polynomial/field_division.lean

deleted theorem polynomial.irreducible_of_monic

Modified src/data/polynomial/monic.lean

deleted theorem polynomial.eq_one_of_is_unit_of_monic

deleted theorem polynomial.is_unit_C

added theorem polynomial.monic.eq_one_of_is_unit

Modified src/data/polynomial/ring_division.lean

modified theorem polynomial.degree_eq_zero_of_is_unit

added theorem polynomial.irreducible_of_monic

modified theorem polynomial.is_unit_iff

added theorem polynomial.nat_degree_eq_zero_of_is_unit

Modified src/field_theory/minpoly.lean