Theorem Nat.ArithmeticFunction.IsMultiplicative.map_prod_of_subset_primeFactors

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.map_prod_of_subset_primeFactors View on Github →

2023-12-27 17:24

Mathlib/NumberTheory/ArithmeticFunction.lean

feat: define `prodPrimeFactors` as an `ArithmeticFunction` (#6662) …

Added Nat.ArithmeticFunction.IsMultiplicative.map_prod_of_subset_primeFactors View on Github →