Theorem Nat.ArithmeticFunction.cardDistinctFactors_eq_cardFactors_iff_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.cardDistinctFactors_eq_cardFactors_iff_squarefree View on Github →

2023-05-30 06:41

Mathlib/NumberTheory/ArithmeticFunction.lean

feat: port NumberTheory.ArithmeticFunction (#4358)

Added Nat.ArithmeticFunction.cardDistinctFactors_eq_cardFactors_iff_squarefree View on Github →