Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-18 09:31 0d3092b6

View on Github →

feat(number_theory/arithmetic_function): defining several more arithmetic_functions (#4998) Defines arithmetic functions card_factors, card_distinct_factors, and moebius

Estimated changes

Modified src/algebra/squarefree.lean

Modified src/number_theory/arithmetic_function.lean

added def nat.arithmetic_function.card_distinct_factors

added theorem nat.arithmetic_function.card_distinct_factors_apply

added theorem nat.arithmetic_function.card_distinct_factors_eq_card_factors_iff_squarefree

added theorem nat.arithmetic_function.card_distinct_factors_zero

added def nat.arithmetic_function.card_factors

added theorem nat.arithmetic_function.card_factors_apply

added theorem nat.arithmetic_function.card_factors_eq_one_iff_prime

added theorem nat.arithmetic_function.card_factors_mul

added theorem nat.arithmetic_function.card_factors_multiset_prod

added def nat.arithmetic_function.moebius

added theorem nat.arithmetic_function.moebius_apply_of_squarefree

added theorem nat.arithmetic_function.moebius_eq_zero_of_not_squarefree

added theorem nat.arithmetic_function.moebius_ne_zero_iff_squarefree

Modified src/ring_theory/multiplicity.lean

added theorem multiplicity.multiplicity_zero_eq_zero_of_ne_zero