Commit 2024-06-15 08:58 f6c43c61

chore/refactor: avoid vector notation in character defs (#13737) This changes the definition of the quadratic character ZMod.χ₄ to use ane explicit match expression instead of ![0, 1, 0, -1] (which relied on defeq abuse ZMod = Fin), and similarly for ZMod.χ₈ and ZMod.χ₈'. We also deal with some porting notes, tidy up some files and speed up Mathlib.NumberTheory.GaussSum.