Theorems · Theorem · number theory

BoundingSieve.inv_selbergTerms_eq_sum_divisors_moebius_nu

∀ {s : BoundingSieve} {l : ℕ},
  Squarefree l →
    s.nu l ≠ 0 →
      (BoundingSieve.selbergTerms l)⁻¹ =
        ∑ x ∈ l.divisorsAntidiagonal,
          match x with
          | (d, e) => ↑(ArithmeticFunction.moebius d) * (s.nu e)⁻¹

Defined in: Mathlib.NumberTheory.SelbergSieve
Cited by: 1 results in Mathlib
Foundations: Depth 107 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites28

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

DFunLike.coestatement and proof · cited by 62,936
Realstatement and proof · cited by 25,697
Finset.sumstatement and proof · cited by 5,195
mul_oneproof · cited by 3,885
one_mulproof · cited by 2,841
Finset.sum_congrproof · cited by 2,323
mul_assocproof · cited by 1,667
one_ne_zeroproof · cited by 885
div_oneproof · cited by 629
inv_invproof · cited by 494
ArithmeticFunctionstatement · cited by 290
mul_inv_revproof · cited by 270

Cited by1

Results whose statement or proof uses this declaration.

BoundingSieve.nu_inv_eq_sum_divisors_inv_selbergTermsproof · cited by 2