Theorem Mathlib.Meta.NormNum.LegendreSym.to_jacobiSym

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.LegendreSym.to_jacobiSym View on Github →