Theorems · Theorem · number theory

ZMod.eisenstein_lemma_aux

∀ (p : ℕ) [inst : Fact (Nat.Prime p)] [Fact (p % 2 = 1)] {a : ℕ},
  a % 2 = 1 →
    ↑a ≠ 0 →
      {x ∈ Finset.Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val}.card ≡ ∑ x ∈ Finset.Ico 1 (p / 2).succ, x * a / p [MOD 2]

Defined in: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Cited by: 1 results in Mathlib
Foundations: Depth 82 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Fact Fact

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites21

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

Finset.sumstatement and proof · cited by 5,195
mul_oneproof · cited by 3,885
Factstatement and proof · cited by 2,726
Nat.cast_oneproof · cited by 2,501
Finset.cardstatement and proof · cited by 2,327
Finset.sum_congrproof · cited by 2,323
mul_commproof · cited by 2,262
Nat.Primestatement and proof · cited by 2,059
ZModstatement · cited by 1,024
sub_eq_add_negproof · cited by 1,023
Finset.filterstatement and proof · cited by 949
add_assocproof · cited by 746

Cited by1

Results whose statement or proof uses this declaration.

ZMod.eisenstein_lemmaproof · cited by 0