Theorems · Definition · number theory
LSeries.convolution
{R : Type u_1} → [Semiring R] → (ℕ → R) → (ℕ → R) → ℕ → RDirichlet convolution of two sequences. We define this in terms of the already existing definition for arithmetic functions.
- Defined in
- Mathlib.NumberTheory.LSeries.Convolution
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 64 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Semiring
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
- Semiringstatement and proof · cited by 13,802
- toArithmeticFunctionproof · cited by 5
Cited by18
Results whose statement or proof uses this declaration.
- ArithmeticFunction.coe_mulstatement · cited by 6
- LSeries_convolution'statement · cited by 5
- LSeries.convolution_defstatement · cited by 4
- LSeriesHasSum.convolutionstatement · cited by 3
- LSeries.convolution_congrstatement · cited by 2
- DirichletCharacter.mul_convolution_distribstatement · cited by 2
- LSeriesSummable.convolutionstatement · cited by 2
- DirichletCharacter.convolution_mul_moebiusstatement and proof · cited by 1
- DirichletCharacter.convolution_twist_vonMangoldtstatement and proof · cited by 1
- LSeries_convolutionstatement · cited by 1
- LSeries.convolution_one_eq_convolution_zetastatement · cited by 1
- LSeries.one_convolution_eq_zeta_convolutionstatement · cited by 1