Eisenstein's lemma

TheoremEisenstein's lemma for Jacobi symbols (odd coprime form)#✓fully proved

Let \(a\) and \(b\) be odd natural numbers that are coprime. Then the Jacobi symbol \(\left(\frac{a}{b}\right)\) equals \((-1)^{S}\), where \(S = \sum_{i=1}^{(b-1)/2} \lfloor ia/b \rfloor\).

theorem eisenstein_lemma_jacobi_symbol_general
    (a b : ℕ) (ha_odd : Odd a) (hb_odd : Odd b) (hab : Nat.Coprime a b) :
    jacobiSym (a : ℤ) b =
      (-1 : ℤ) ^ ∑ i ∈ Finset.Icc 1 ((b - 1) / 2), (i * a) / b

Used by 1

Used byEisenstein's lemma for Jacobi symbols

TheoremEisenstein's lemma for Jacobi symbols#✓fully proved

Let \(a\) and \(b\) be positive odd natural numbers that are coprime. Then the Jacobi symbol \(\left(\frac{a}{b}\right)\) equals \((-1)^{S}\), where \(S = \sum_{i=1}^{(b-1)/2} \lfloor ia/b \rfloor\).

theorem eisenstein_lemma_jacobi_symbol
    (a b : ℕ) (ha_pos : 0 < a) (hb_pos : 0 < b)
    (ha_odd : Odd a) (hb_odd : Odd b) (hab : Nat.Coprime a b) :
    jacobiSym (a : ℤ) b =
      (-1 : ℤ) ^ ∑ i ∈ Finset.Icc 1 ((b - 1) / 2), (i * a) / b

Sources

• Damanvir Singh Binner, "Generalization of a Result of Sylvester Related to the Frobenius Coin Problem", Journal of Integer Sequences 24 (2021), Article 21.8.4, Theorem Eisenstein, lines 272-278, https://cs.uwaterloo.ca/journals/JIS/VOL24/Binner/binner13.tex. It follows from eisenstein_lemma_jacobi_symbol_general; the hypotheses ha_pos and hb_pos are unused and keep the source's shape.

Uses 1

Proof usesEisenstein's lemma for Jacobi symbols (odd coprime form)

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.