Def AddChar.zmodChar

Modification history

2024-06-17 11:20

Mathlib/NumberTheory/LegendreSymbol/AddCharacter.lean

chore(NumberTheory/MulChar): deprecate `IsNontrivial`, fix `isPrimitive` (#13878) …

Modified AddChar.zmodChar View on Github →

2023-06-23 06:08

Mathlib/NumberTheory/LegendreSymbol/AddCharacter.lean

feat: port NumberTheory.LegendreSymbol.AddCharacter (#5397)

Added AddChar.zmodChar View on Github →