Commit 2023-06-29 13:10 c0cf4ad2

View on Github →

feat: port number_theory.legendre_symbol.norm_num to Tactic.NormNum.LegendreSymbol (#5548)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Tactic.lean

Created Mathlib/Tactic/NormNum/LegendreSymbol.lean

added theorem Mathlib.Meta.NormNum.JacobiSym.mod_left

added theorem Mathlib.Meta.NormNum.LegendreSym.to_jacobiSym

added theorem Mathlib.Meta.NormNum.isInt_jacobiSym

added theorem Mathlib.Meta.NormNum.isInt_jacobiSymNat

added theorem Mathlib.Meta.NormNum.jacobiSymNat.double_even

added theorem Mathlib.Meta.NormNum.jacobiSymNat.even_even

added theorem Mathlib.Meta.NormNum.jacobiSymNat.even_odd₁

added theorem Mathlib.Meta.NormNum.jacobiSymNat.even_odd₃

added theorem Mathlib.Meta.NormNum.jacobiSymNat.even_odd₅

added theorem Mathlib.Meta.NormNum.jacobiSymNat.even_odd₇

added theorem Mathlib.Meta.NormNum.jacobiSymNat.mod_left

added theorem Mathlib.Meta.NormNum.jacobiSymNat.odd_even

added theorem Mathlib.Meta.NormNum.jacobiSymNat.one_left

added theorem Mathlib.Meta.NormNum.jacobiSymNat.one_right

added theorem Mathlib.Meta.NormNum.jacobiSymNat.qr₁'

added theorem Mathlib.Meta.NormNum.jacobiSymNat.qr₁'_mod

added theorem Mathlib.Meta.NormNum.jacobiSymNat.qr₁

added theorem Mathlib.Meta.NormNum.jacobiSymNat.qr₁_mod

added theorem Mathlib.Meta.NormNum.jacobiSymNat.qr₃

added theorem Mathlib.Meta.NormNum.jacobiSymNat.qr₃_mod

added theorem Mathlib.Meta.NormNum.jacobiSymNat.zero_left

added theorem Mathlib.Meta.NormNum.jacobiSymNat.zero_right

added def Mathlib.Meta.NormNum.jacobiSymNat

added def Tactic.NormNum.evalJacobiSym

added def Tactic.NormNum.evalJacobiSymNat

added def Tactic.NormNum.evalLegendreSym

Modified test/norm_num_ext.lean