Theorem Nat.ArithmeticFunction.IsMultiplicative.prodPrimeFactors_one_add_of_squarefree

Modification history

2024-02-10 13:10
Mathlib/NumberTheory/ArithmeticFunction.lean
chore(NumberTheory/ArithmeticFunction): remove `Nat.` part from `ArithmeticFunction` namespace (#10399) …
Deleted Nat.ArithmeticFunction.IsMultiplicative.prodPrimeFactors_one_add_of_squarefreeView on Github →
2023-12-27 17:24
Mathlib/NumberTheory/ArithmeticFunction.lean
feat: define `prodPrimeFactors` as an `ArithmeticFunction` (#6662) …
Added Nat.ArithmeticFunction.IsMultiplicative.prodPrimeFactors_one_add_of_squarefreeView on Github →