Theorem ArithmeticFunction.cardDistinctFactors_apply

Modification history

2024-07-17 17:39

Mathlib/NumberTheory/ArithmeticFunction.lean

chore: Rename `Nat.factors` to `Nat.primeFactorsList` (#13832) …

Modified ArithmeticFunction.cardDistinctFactors_apply View on Github →

2024-02-10 13:10

Mathlib/NumberTheory/ArithmeticFunction.lean

chore(NumberTheory/ArithmeticFunction): remove `Nat.` part from `ArithmeticFunction` namespace (#10399) …

Added ArithmeticFunction.cardDistinctFactors_apply View on Github →