Theorems · Definition · number theory
ArithmeticFunction.vonMangoldt
ArithmeticFunction ℝ
The vonMangoldt function is the function on natural numbers that returns log p if the input can
be expressed as p^k for a prime p.
In the case when n is a prime power, Nat.minFac will give the appropriate prime, as it is the
smallest prime factor.
In the ArithmeticFunction locale, we have the notation Λ for this function.
This is also available in the ArithmeticFunction.vonMangoldt locale, allowing for selective
access to the notation.
- Cited by
- 40 results in Mathlib
- Foundations
- Depth 170 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement · cited by 25,697
- Real.logproof · cited by 939
- ArithmeticFunctionstatement · cited by 290
- IsPrimePowproof · cited by 77
- Nat.minFacproof · cited by 72
Cited by42
Results whose statement or proof uses this declaration.
- Chebyshev.psiproof · cited by 34
- ArithmeticFunction.vonMangoldt.residueClassproof · cited by 14
- Chebyshev.psi_eq_zero_of_lt_twoproof · cited by 7
- ArithmeticFunction.vonMangoldt_nonnegstatement · cited by 6
- ArithmeticFunction.vonMangoldt_apply_onestatement · cited by 4
- ArithmeticFunction.vonMangoldt_apply_primestatement · cited by 4
- ArithmeticFunction.vonMangoldt_apply_powstatement · cited by 3
- ArithmeticFunction.vonMangoldt_mul_zetastatement · cited by 3
- ArithmeticFunction.vonMangoldt_ne_zero_iffstatement · cited by 3
- DirichletCharacter.LSeriesSummable_twist_vonMangoldtstatement · cited by 2
- DirichletCharacter.LSeries_twist_vonMangoldt_eqstatement and proof · cited by 2
- ArithmeticFunction.vonMangoldt.abscissaOfAbsConv_residueClass_le_oneproof · cited by 2