Theorem Mathlib.Meta.NormNum.jacobiSymNat.even_odd₃

Modification history

2023-06-29 13:10

Mathlib/Tactic/NormNum/LegendreSymbol.lean

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

Added Mathlib.Meta.NormNum.jacobiSymNat.even_odd₃ View on Github →