Theorem ZMod.χ₈_int_mod_eight

Modification history

2023-05-22 19:15

Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean

feat: port NumberTheory.LegendreSymbol.ZModChar (#4205)

Added ZMod.χ₈_int_mod_eight View on Github →