Power residues and reciprocity

Quadratic and cubic residues, Legendre, Jacobi and Kronecker symbols, quadratic reciprocity and its extensions, Legendre-symbol sums.

• Cubic residue symbol
• Eisenstein's lemma
• Kronecker symbol and quadratic characters
• Squares modulo powers of two

TheoremLinear Legendre-symbol sums vanish#✓fully proved

Let \(p\) be an odd prime and let \(b\) and \(c\) be integers with \(p \nmid b\). Then the Legendre symbols \(\left(\frac{b\ell + c}{p}\right)\) for \(\ell = 0, 1, \dots, p - 1\) sum to \(0\).

public theorem sum_linear_eq_zero
    (p : ℕ) [Fact p.Prime] (hpodd : Odd p) (b c : ℤ) (hb : ¬ (p : ℤ) ∣ b) :
    ∑ ℓ ∈ Finset.range p, legendreSym p (b * (ℓ : ℤ) + c) = 0

Sources

• This is the first corollary of Theorem thm1 in Ram Krishna Pandey and Anshumaan Parashar, On Certain Sums with Quadratic Expressions Involving the Legendre Symbol, Journal of Integer Sequences 21 (2018), Article 18.4.7, lines 190–193, https://cs.uwaterloo.ca/journals/JIS/VOL21/Pandey/pandey14.tex. The proof here reindexes Mathlib's quadraticChar_sum_zero through the affine permutation x ↦ b * x + c of ZMod p.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.