Theorems · Definition · number theory
ArithmeticFunction.natToArithmeticFunction
{R : Type u_1} → [inst : AddMonoidWithOne R] → ArithmeticFunction ℕ → ArithmeticFunction RCoerce an arithmetic function with values in ℕ to one with values in R. We cannot inline
this in natCoe because it gets unfolded too much.
- Cited by
- 30 results in Mathlib
- Foundations
- Depth 24 from the axioms · uses propext
- Assumes
- AddMonoidWithOne
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- AddMonoidWithOnestatement and proof · cited by 313
- ArithmeticFunctionstatement and proof · cited by 290
Cited by33
Results whose statement or proof uses this declaration.
- ArithmeticFunction.ppowproof · cited by 6
- DirichletCharacter.zetaMulproof · cited by 4
- ArithmeticFunction.IsMultiplicative.natCaststatement · cited by 4
- ArithmeticFunction.coe_mul_zeta_applystatement · cited by 4
- ArithmeticFunction.coe_zeta_mul_applystatement · cited by 4
- ArithmeticFunction.moebius_mul_coe_zetastatement and proof · cited by 4
- ArithmeticFunction.natCoe_natstatement and proof · cited by 4
- ArithmeticFunction.ppow_zerostatement and proof · cited by 3
- ArithmeticFunction.coe_zeta_mul_coe_moebiusstatement · cited by 3
- ArithmeticFunction.coe_zeta_smul_applystatement · cited by 3
- ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eqproof · cited by 3
- ArithmeticFunction.vonMangoldt_mul_zetastatement · cited by 3