Commit 2025-11-13 11:49 68f2d7d8

View on Github →

feat: add cardDistinctFactors lemmas (#31585)

Estimated changes

Modified Mathlib/NumberTheory/ArithmeticFunction.lean

added theorem ArithmeticFunction.cardDistinctFactors_eq_one_iff

added theorem ArithmeticFunction.cardDistinctFactors_mul

added theorem ArithmeticFunction.cardDistinctFactors_prod