mathlib3

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

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](https://leanprover-community.github.io/mathlib_docs/data/mv_polynomial/basic.html#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*. Co-authored-by: Thomas Browning <thomas.l.browning@gmail.com> Co-authored-by: Anne Baanen <t.baanen@vu.nl> Inspired by #17631