Theorem Mathlib.Meta.NormNum.jacobiSymNat.qr₁'

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.qr₁'View on Github →