Theorem gaussSum_sq

Modification history

2024-06-17 11:20

Mathlib/NumberTheory/GaussSum.lean

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

Modified gaussSum_sq View on Github →

2024-06-14 14:02

Mathlib/NumberTheory/GaussSum.lean

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

Modified gaussSum_sq View on Github →

2023-06-26 10:09

Mathlib/NumberTheory/LegendreSymbol/GaussSum.lean

feat: port NumberTheory.LegendreSymbol.GaussSum (#5419) …

Added gaussSum_sq View on Github →