Theorems · Definition · number theory
ArithmeticFunction.ofInt
{R : Type u_1} → [inst : AddGroupWithOne R] → ArithmeticFunction ℤ → ArithmeticFunction RCoerce an arithmetic function with values in ℤ to one with values in R. We cannot inline
this in intCoe because it gets unfolded too much.
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 40 from the axioms · uses propext
- Assumes
- AddGroupWithOne
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
- ArithmeticFunctionstatement and proof · cited by 290
- AddGroupWithOnestatement and proof · cited by 111
Cited by15
Results whose statement or proof uses this declaration.
- ArithmeticFunction.coe_zeta_mul_coe_moebiusstatement and proof · cited by 3
- ArithmeticFunction.intCoe_mulstatement · cited by 2
- ArithmeticFunction.intCoe_onestatement · cited by 2
- ArithmeticFunction.zetaUnitproof · cited by 2
- ArithmeticFunction.coe_coestatement · cited by 2
- ArithmeticFunction.LSeries_zeta_mul_Lseries_moebiusproof · cited by 2
- DirichletCharacter.convolution_mul_moebiusproof · cited by 1
- ArithmeticFunction.intCoe_applystatement · cited by 1
- ArithmeticFunction.IsMultiplicative.intCaststatement · cited by 1
- ArithmeticFunction.log_mul_moebius_eq_vonMangoldtstatement and proof · cited by 1
- ArithmeticFunction.intCoe_intstatement · cited by 0
- ArithmeticFunction.inv_zetaUnitstatement · cited by 0