Commit 2022-12-06 17:02 fa256f00

feat(data/polynomial): irreducibility criteria for (quadratic) monic polynomials (#17664)

To show a monic polynomial p over a commutative semiring without zero divisors is irreducible, it suffices to show that p ≠ 1 and that there doesn't exist a factorization into the product of two monic polynomials of positive degrees: monic.irreducible_iff_nat_degree.
If such a factorization exists, one of the polynomial must have degree less than or equal to p.nat_degree / 2: monic.irreducible_iff_nat_degree'.
To show a quadratic monic polynomial p is reducible, it suffices to it doesn't factor as (X+c)(X+c'), i.e. there don't exist c and c' that add up to the 1st coefficient and multiply up to the 0th coefficient: not_irreducible_iff_exists_add_mul_eq_coeff.
Define the ring homomorphism constant_coeff in coeff.lean which is analogous to mv_polynomial.constant_coeff; use it to golf and generalize is_unit_C and eq_one_of_is_unit_of_monic in monic.lean and various lemmas in ring_division.lean.
Add monic.is_unit_iff.
Golf some lemmas in erase_lead.lean. Inspired by #17631