Theorem MulChar.IsQuadratic.gaussSum_frob_iter

Modification history

2023-06-26 10:09
Mathlib/NumberTheory/LegendreSymbol/GaussSum.lean
feat: port NumberTheory.LegendreSymbol.GaussSum (#5419) …
Added MulChar.IsQuadratic.gaussSum_frob_iterView on Github →