LegendreSymbol

📁 Source: Mathlib/Tactic/NormNum/LegendreSymbol.lean

Statistics

Metric	Count
Definitions jacobiSymNat, proveJacobiSym, proveJacobiSymNat, proveJacobiSymOdd, evalJacobiSym, evalJacobiSymNat, evalLegendreSym	7
Theorems mod_left, to_jacobiSym, isInt_jacobiSym, isInt_jacobiSymNat, double_even, even_even, even_odd₁, even_odd₃, even_odd₅, even_odd₇, mod_left, odd_even, one_left, one_right, qr₁, qr₁', qr₁'_mod, qr₁_mod, qr₃, qr₃_mod, zero_left, zero_right	22
Total	29

Mathlib.Meta.NormNum

Definitions

Name	Category	Theorems
jacobiSymNat 📖	CompOp	5 math math: jacobiSymNat.even_even, jacobiSymNat.zero_left, jacobiSymNat.zero_right, jacobiSymNat.one_right, jacobiSymNat.one_left
proveJacobiSym 📖	CompOp	—
proveJacobiSymNat 📖	CompOp	—
proveJacobiSymOdd 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isInt_jacobiSym 📖	—	IsInt Int.instRing IsNat Nat.instAddMonoidWithOne jacobiSym	—	—	—
isInt_jacobiSymNat 📖	mathematical	IsNat Nat.instAddMonoidWithOne jacobiSymNat	IsInt Int.instRing	—	—

Mathlib.Meta.NormNum.JacobiSym

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mod_left 📖	mathematical	Mathlib.Meta.NormNum.jacobiSymNat	jacobiSym	—	jacobiSym.mod_left

Mathlib.Meta.NormNum.LegendreSym

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
to_jacobiSym 📖	mathematical	Mathlib.Meta.NormNum.IsInt Int.instRing jacobiSym	legendreSym	—	jacobiSym.legendreSym.to_jacobiSym

Mathlib.Meta.NormNum.jacobiSymNat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
double_even 📖	—	Mathlib.Meta.NormNum.jacobiSymNat	—	—	Nat.instAtLeastTwoHAddOfNat jacobiSym.div_four_left Nat.cast_zero Int.instCharZero
even_even 📖	mathematical	—	Mathlib.Meta.NormNum.jacobiSymNat	—	jacobiSym.eq_zero_iff ne_of_gt LT.lt.trans_le Nat.not_even_one Nat.instAtLeastTwoHAddOfNat even_iff_two_dvd
even_odd₁ 📖	—	Mathlib.Meta.NormNum.jacobiSymNat	—	—	Nat.instAtLeastTwoHAddOfNat jacobiSym.even_odd Nat.cast_zero Int.instCharZero Nat.instCharZero
even_odd₃ 📖	—	Mathlib.Meta.NormNum.jacobiSymNat	—	—	Nat.instAtLeastTwoHAddOfNat jacobiSym.even_odd Nat.cast_zero Int.instCharZero
even_odd₅ 📖	—	Mathlib.Meta.NormNum.jacobiSymNat	—	—	Nat.instAtLeastTwoHAddOfNat jacobiSym.even_odd Nat.cast_zero Int.instCharZero
even_odd₇ 📖	—	Mathlib.Meta.NormNum.jacobiSymNat	—	—	Nat.instAtLeastTwoHAddOfNat jacobiSym.even_odd Nat.cast_zero Int.instCharZero
mod_left 📖	—	Mathlib.Meta.NormNum.jacobiSymNat	—	—	jacobiSym.mod_left
odd_even 📖	—	Mathlib.Meta.NormNum.jacobiSymNat	—	—	Nat.fact_prime_two legendreSym.mod legendreSym.congr_simp eq_or_ne jacobiSym.mul_right jacobiSym.legendreSym.to_jacobiSym one_mul
one_left 📖	mathematical	—	Mathlib.Meta.NormNum.jacobiSymNat	—	Nat.cast_one jacobiSym.one_left
one_right 📖	mathematical	—	Mathlib.Meta.NormNum.jacobiSymNat	—	jacobiSym.one_right
qr₁ 📖	—	Mathlib.Meta.NormNum.jacobiSymNat	—	—	jacobiSym.quadratic_reciprocity_one_mod_four Nat.odd_iff
qr₁' 📖	—	Mathlib.Meta.NormNum.jacobiSymNat	—	—	jacobiSym.quadratic_reciprocity_one_mod_four Nat.odd_iff
qr₁'_mod 📖	—	Mathlib.Meta.NormNum.jacobiSymNat	—	—	qr₁' mod_left
qr₁_mod 📖	—	Mathlib.Meta.NormNum.jacobiSymNat	—	—	qr₁ mod_left
qr₃ 📖	—	Mathlib.Meta.NormNum.jacobiSymNat	—	—	jacobiSym.quadratic_reciprocity_three_mod_four
qr₃_mod 📖	—	Mathlib.Meta.NormNum.jacobiSymNat	—	—	qr₃ mod_left
zero_left 📖	mathematical	—	Mathlib.Meta.NormNum.jacobiSymNat	—	Nat.cast_zero jacobiSym.zero_left
zero_right 📖	mathematical	—	Mathlib.Meta.NormNum.jacobiSymNat	—	jacobiSym.zero_right

Tactic.NormNum

Definitions

Name	Category	Theorems
evalJacobiSym 📖	CompOp	—
evalJacobiSymNat 📖	CompOp	—
evalLegendreSym 📖	CompOp	—

---

← Back to Index