Theorems · Theorem · number theory
ArithmeticFunction.IsMultiplicative.natCast
∀ {R : Type u_1} {f : ArithmeticFunction ℕ} [inst : Semiring R], f.IsMultiplicative → (↑f).IsMultiplicative- Cited by
- 4 results in Mathlib
- Foundations
- Depth 28 from the axioms · uses propext
- Assumes
- Semiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Semiringstatement and proof · cited by 13,802
- Nat.cast_oneproof · cited by 2,501
- Nat.cast_mulproof · cited by 309
- ArithmeticFunctionstatement and proof · cited by 290
- ArithmeticFunction.IsMultiplicativestatement and proof · cited by 45
- ArithmeticFunction.natToArithmeticFunctionstatement · cited by 30
- ArithmeticFunction.IsMultiplicative.map_oneproof · cited by 8
Cited by4
Results whose statement or proof uses this declaration.
- ArithmeticFunction.moebius_mul_coe_zetaproof · cited by 4
- ArithmeticFunction.IsMultiplicative.ppowproof · cited by 1
- DirichletCharacter.isMultiplicative_zetaMulproof · cited by 1