Theorem UniqueFactorizationMonoid.prod_normalizedFactors

Modification history

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