Theorems · Definition · number theory
ArithmeticFunction.moebius
ArithmeticFunction ℤ
μ is the Möbius function. If n is squarefree with an even number of distinct prime factors,
μ n = 1. If n is squarefree with an odd number of distinct prime factors, μ n = -1.
If n is not squarefree, μ n = 0.
- Cited by
- 45 results in Mathlib
- Foundations
- Depth 82 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- ArithmeticFunctionstatement · cited by 290
- Squarefreeproof · cited by 112
- ArithmeticFunction.cardFactorsproof · cited by 22
Cited by46
Results whose statement or proof uses this declaration.
- ArithmeticFunction.moebius_apply_of_squarefreestatement · cited by 7
- ArithmeticFunction.moebius_eq_zero_of_not_squarefreestatement · cited by 4
- ArithmeticFunction.moebius_mul_coe_zetastatement and proof · cited by 4
- ArithmeticFunction.coe_zeta_mul_coe_moebiusstatement and proof · cited by 3
- ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eqstatement and proof · cited by 3
- ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq_onstatement and proof · cited by 3
- ArithmeticFunction.moebius_apply_primestatement · cited by 3
- DirichletCharacter.LSeries_ne_zero_of_one_lt_reproof · cited by 2
- ArithmeticFunction.coe_zeta_mul_moebiusstatement and proof · cited by 2
- ArithmeticFunction.isMultiplicative_moebiusstatement · cited by 2
- ArithmeticFunction.LSeriesSummable_moebius_iffstatement and proof · cited by 2
- ArithmeticFunction.zetaUnitproof · cited by 2