Commit 2024-02-15 16:16 f23db5ad

View on Github →

feat: add some simple results regarding polynomials (#10572)

  • Polynomial.map_contract: Polynomial.map and Polynomial.contract commutes
  • Irreducible.natDegree_pos: an irreducible polynomial over a field must have positive degree (not true if it's not a field)
  • Polynomial.Monic.nextCoeff_pow: corollary of Polynomial.Monic.nextCoeff_mul
  • Polynomial.exists_monic_irreducible_factor: a polynomial over a field which is not a unit must have a monic irreducible factor (not true if it's not a field)

Estimated changes