Theorem ArithmeticFunction.cardDistinctFactors_eq_one_iff

Modification history

2025-12-02 09:01
Mathlib/NumberTheory/ArithmeticFunction.lean
refactor(NumberTheory/ArithmeticFunction): split long file (#32304) …
Modified ArithmeticFunction.cardDistinctFactors_eq_one_iffView on Github →
2025-11-13 11:49
Mathlib/NumberTheory/ArithmeticFunction.lean
feat: add cardDistinctFactors lemmas (#31585)
Added ArithmeticFunction.cardDistinctFactors_eq_one_iffView on Github →