Theorem Polynomial.leadingCoeff_mul_prod_normalizedFactors

Modification history

2024-12-16 11:07
Mathlib/Algebra/Polynomial/FieldDivision.lean
feat(Algebra/Polynomial/FieldDivision): factoring polynomials to irreducible monic factors (#19640)
Added Polynomial.leadingCoeff_mul_prod_normalizedFactorsView on Github →