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 →