Def AddChar.IsPrimitive

Modification history

2024-06-14 14:02

Mathlib/NumberTheory/LegendreSymbol/AddCharacter.lean

feat(AddChar): Various improvements (#13579) …

Modified AddChar.IsPrimitive View on Github →

2023-06-23 06:08

Mathlib/NumberTheory/LegendreSymbol/AddCharacter.lean

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

Added AddChar.IsPrimitive View on Github →