Theorem Nat.prod_primeFactors_sdiff_of_squarefree

Modification history

2023-12-27 17:24
Mathlib/Data/Nat/Squarefree.lean
feat: define `prodPrimeFactors` as an `ArithmeticFunction` (#6662) …
Added Nat.prod_primeFactors_sdiff_of_squarefreeView on Github →