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

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