Database BASIC REAL AND COMPLEX FUNCTIONS Basic number theory Quadratic residues and the Legendre symbol lgsval2
Description: The Legendre symbol at a prime (this is the traditional domain of the
Legendre symbol, except for the addition of prime 2 ). (Contributed by Mario Carneiro , 4-Feb-2015)
Ref
Expression
Assertion
lgsval2 ⊢ A ∈ ℤ ∧ P ∈ ℙ → A / L P = if P = 2 if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1 A P − 1 2 + 1 mod P − 1
Proof
Step
Hyp
Ref
Expression
1
eqid ⊢ n ∈ ℕ ⟼ if n ∈ ℙ if n = 2 if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1 A n − 1 2 + 1 mod n − 1 n pCnt P 1 = n ∈ ℕ ⟼ if n ∈ ℙ if n = 2 if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1 A n − 1 2 + 1 mod n − 1 n pCnt P 1
2
1
lgsval2lem ⊢ A ∈ ℤ ∧ P ∈ ℙ → A / L P = if P = 2 if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1 A P − 1 2 + 1 mod P − 1