Documentation Verification Report

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	19 math math: `jacobiSymNat.even_odd₁`, `jacobiSymNat.double_even`, `jacobiSymNat.even_odd₇`, `jacobiSymNat.even_even`, `jacobiSymNat.zero_left`, `jacobiSymNat.even_odd₃`, `jacobiSymNat.zero_right`, `jacobiSymNat.qr₃_mod`, `jacobiSymNat.mod_left`, `jacobiSymNat.qr₁'`, `jacobiSymNat.qr₁`, `isInt_jacobiSymNat`, `jacobiSymNat.one_right`, `jacobiSymNat.even_odd₅`, `jacobiSymNat.qr₃`, `jacobiSymNat.odd_even`, `jacobiSymNat.one_left`, `jacobiSymNat.qr₁_mod`, `jacobiSymNat.qr₁'_mod`
`proveJacobiSym` 📖	CompOp	—
`proveJacobiSymNat` 📖	CompOp	—
`proveJacobiSymOdd` 📖	CompOp	—

Theorems

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

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`	`Mathlib.Meta.NormNum.IsInt` `Int.instRing` `legendreSym`	—	`jacobiSym.legendreSym.to_jacobiSym`

Mathlib.Meta.NormNum.jacobiSymNat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`double_even` 📖	mathematical	`Mathlib.Meta.NormNum.jacobiSymNat`	`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₁` 📖	mathematical	`Mathlib.Meta.NormNum.jacobiSymNat`	`Mathlib.Meta.NormNum.jacobiSymNat`	—	`Nat.instAtLeastTwoHAddOfNat` `jacobiSym.even_odd` `Nat.cast_zero` `Int.instCharZero` `Nat.instCharZero`
`even_odd₃` 📖	mathematical	`Mathlib.Meta.NormNum.jacobiSymNat`	`Mathlib.Meta.NormNum.jacobiSymNat`	—	`Nat.instAtLeastTwoHAddOfNat` `jacobiSym.even_odd` `Nat.cast_zero` `Int.instCharZero`
`even_odd₅` 📖	mathematical	`Mathlib.Meta.NormNum.jacobiSymNat`	`Mathlib.Meta.NormNum.jacobiSymNat`	—	`Nat.instAtLeastTwoHAddOfNat` `jacobiSym.even_odd` `Nat.cast_zero` `Int.instCharZero`
`even_odd₇` 📖	mathematical	`Mathlib.Meta.NormNum.jacobiSymNat`	`Mathlib.Meta.NormNum.jacobiSymNat`	—	`Nat.instAtLeastTwoHAddOfNat` `jacobiSym.even_odd` `Nat.cast_zero` `Int.instCharZero`
`mod_left` 📖	mathematical	`Mathlib.Meta.NormNum.jacobiSymNat`	`Mathlib.Meta.NormNum.jacobiSymNat`	—	`jacobiSym.mod_left`
`odd_even` 📖	mathematical	`Mathlib.Meta.NormNum.jacobiSymNat`	`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₁` 📖	mathematical	`Mathlib.Meta.NormNum.jacobiSymNat`	`Mathlib.Meta.NormNum.jacobiSymNat`	—	`jacobiSym.quadratic_reciprocity_one_mod_four` `Nat.odd_iff`
`qr₁'` 📖	mathematical	`Mathlib.Meta.NormNum.jacobiSymNat`	`Mathlib.Meta.NormNum.jacobiSymNat`	—	`jacobiSym.quadratic_reciprocity_one_mod_four` `Nat.odd_iff`
`qr₁'_mod` 📖	mathematical	`Mathlib.Meta.NormNum.jacobiSymNat`	`Mathlib.Meta.NormNum.jacobiSymNat`	—	`qr₁'` `mod_left`
`qr₁_mod` 📖	mathematical	`Mathlib.Meta.NormNum.jacobiSymNat`	`Mathlib.Meta.NormNum.jacobiSymNat`	—	`qr₁` `mod_left`
`qr₃` 📖	mathematical	`Mathlib.Meta.NormNum.jacobiSymNat`	`Mathlib.Meta.NormNum.jacobiSymNat`	—	`jacobiSym.quadratic_reciprocity_three_mod_four`
`qr₃_mod` 📖	mathematical	`Mathlib.Meta.NormNum.jacobiSymNat`	`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