Commit 2024-12-16 11:07 e8b45bff

View on Github →

feat(Algebra/Polynomial/FieldDivision): factoring polynomials to irreducible monic factors (#19640)

Estimated changes

Modified Mathlib/Algebra/Polynomial/FieldDivision.lean

added theorem Polynomial.leadingCoeff_mul_prod_normalizedFactors

Modified Mathlib/Data/Nat/Squarefree.lean

Modified Mathlib/NumberTheory/KummerDedekind.lean

Modified Mathlib/RingTheory/ChainOfDivisors.lean

Modified Mathlib/RingTheory/DedekindDomain/Ideal.lean

Modified Mathlib/RingTheory/Radical.lean

Modified Mathlib/RingTheory/UniqueFactorizationDomain/Finite.lean

Modified Mathlib/RingTheory/UniqueFactorizationDomain/Multiplicative.lean

Modified Mathlib/RingTheory/UniqueFactorizationDomain/Multiplicity.lean

Modified Mathlib/RingTheory/UniqueFactorizationDomain/Nat.lean

Modified Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean

deleted theorem UniqueFactorizationMonoid.normalizedFactors_prod

added theorem UniqueFactorizationMonoid.prod_normalizedFactors

added theorem UniqueFactorizationMonoid.prod_normalizedFactors_eq