Commit 2023-11-22 15:18 029b3d78

View on Github →

feat: Squarefree lemmas for Nat (#8323)

Estimated changes

Modified Mathlib/Data/Nat/Order/Lemmas.lean

Modified Mathlib/Data/Nat/Squarefree.lean

deleted theorem Nat.Squarefree.factorization_le_one

added theorem Nat.factorization_eq_one_of_squarefree

added theorem Nat.primeFactors_div_gcd

added theorem Nat.primeFactors_prod

added theorem Nat.prod_primeFactors_invOn_squarefree

added theorem Nat.prod_primeFactors_of_squarefree

added theorem Squarefree.natFactorization_le_one

Modified Mathlib/NumberTheory/SumTwoSquares.lean