Theorem MulChar.IsQuadratic.gaussSum_frob

Modification history

2024-06-10 04:35
Mathlib/NumberTheory/GaussSum.lean
refactor: move GaussSum directly under NumberTheory (#13540) …
Added MulChar.IsQuadratic.gaussSum_frobView on Github →