Theorems · Theorem · number theory

ZMod.pow_div_two_eq_neg_one_or_one

∀ (p : ℕ) [inst : Fact (Nat.Prime p)] {a : ZMod p}, a ≠ 0 → a ^ (p / 2) = 1 ∨ a ^ (p / 2) = -1

If a : ZMod p is nonzero, then a^(p/2) is either 1 or -1.

Defined in

Mathlib.NumberTheory.LegendreSymbol.Basic

Cited by

0 results in Mathlib

Foundations

Depth 100 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Fact