Theorems · Theorem · number theory

ArithmeticFunction.vonMangoldt.LFunctionResidueClassAux_real

∀ {q : ℕ} {a : ZMod q} [inst : NeZero q],
  IsUnit a →
    ∀ {x : ℝ},
      1 < x →
        ArithmeticFunction.vonMangoldt.LFunctionResidueClassAux a ↑x =
          ↑(ArithmeticFunction.vonMangoldt.LFunctionResidueClassAux a ↑x).re

The auxiliary function takes real values for real arguments x > 1.

Defined in: Mathlib.NumberTheory.LSeries.PrimesInAP
Cited by: 1 results in Mathlib
Foundations: Depth 319 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: NeZero

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites33

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Realstatement and proof · cited by 25,697
Complexstatement and proof · cited by 5,565
Nat.cast_oneproof · cited by 2,501
SummationFilter.unconditionalproof · cited by 2,068
Complex.ofRealstatement and proof · cited by 1,654
IsUnitstatement and proof · cited by 1,602
tsumproof · cited by 1,148
eq_or_neproof · cited by 1,117
ZModstatement and proof · cited by 1,024
Complex.restatement and proof · cited by 882
LE.le.trans_ltproof · cited by 795
ERealproof · cited by 793

Cited by1

Results whose statement or proof uses this declaration.

ArithmeticFunction.vonMangoldt.LSeries_residueClass_lower_boundproof · cited by 1