Theorems · Theorem · number theory
ArithmeticFunction.moebius_mul_coe_zeta
ArithmeticFunction.moebius * ↑ArithmeticFunction.zeta = 1
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 96 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites38
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- mul_oneproof · cited by 3,885
- Nat.cast_oneproof · cited by 2,501
- Finset.sum_congrproof · cited by 2,323
- MulZeroClass.mul_zeroproof · cited by 2,091
- Nat.Primeproof · cited by 2,059
- Nat.cast_zeroproof · cited by 1,870
- LT.lt.ne'proof · cited by 1,417
- Finset.rangeproof · cited by 1,341
- pow_zeroproof · cited by 1,094
- ArithmeticFunctionstatement · cited by 290
- neg_add_cancelproof · cited by 256
Cited by4
Results whose statement or proof uses this declaration.
- ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eqproof · cited by 3
- ArithmeticFunction.coe_zeta_mul_moebiusproof · cited by 2
- ArithmeticFunction.coe_moebius_mul_coe_zetaproof · cited by 0
- ArithmeticFunction.sum_moebius_mul_log_eqproof · cited by 0