feat(NumberTheory/GaussSum): add shift and conjugation lemmas (#39459)

Author: yuanyi-350

Mathlib/NumberTheory/DirichletCharacter/GaussSum.lean

@@ -40,10 +40,8 @@ lemma factorsThrough_of_gaussSum_ne_zero [IsDomain R] {χ : DirichletCharacter R
     (hd : d ∣ N) (he : e.mulShift d = 1) (h_ne : gaussSum χ e ≠ 0) :
     χ.FactorsThrough d := by
   rw [DirichletCharacter.factorsThrough_iff_ker_unitsMap hd]
-  intro u hu
-  rw [MonoidHom.mem_ker, ← Units.val_inj, MulChar.coe_toUnitHom]
-  simpa only [Units.val_one, ne_eq, h_ne, not_false_eq_true, mul_eq_right₀] using
-    gaussSum_aux_of_mulShift e χ hd he hu
+  intro _ hu
+  simpa [← Units.val_inj, h_ne] using gaussSum_aux_of_mulShift e χ hd he hu
 
 /-- If `χ` is primitive, but `e` is not, then `gaussSum χ e = 0`. -/
 lemma gaussSum_eq_zero_of_isPrimitive_of_not_isPrimitive [IsDomain R]
@@ -60,7 +58,6 @@ lemma gaussSum_mulShift_of_isPrimitive [IsDomain R] {χ : DirichletCharacter R N
     (hχ : IsPrimitive χ) (a : ZMod N) :
     gaussSum χ (e.mulShift a) = χ⁻¹ a * gaussSum χ e := by
   by_cases ha : IsUnit a
-  · conv_rhs => rw [← gaussSum_mulShift χ e ha.unit]
-    rw [IsUnit.unit_spec, MulChar.inv_apply_eq_inv, Ring.inverse_mul_cancel_left _ _ (ha.map χ)]
+  · simpa [ha.unit_spec] using gaussSum_mulShift_eq χ e ha.unit
   · rw [MulChar.map_nonunit _ ha, zero_mul]
     exact gaussSum_eq_zero_of_isPrimitive_of_not_isPrimitive _ hχ (not_isPrimitive_mulShift e ha)

Mathlib/NumberTheory/GaussSum.lean

@@ -9,6 +9,8 @@ public import Mathlib.NumberTheory.LegendreSymbol.AddCharacter
 public import Mathlib.NumberTheory.LegendreSymbol.ZModChar
 public import Mathlib.Algebra.CharP.CharAndCard
 
+import Mathlib.NumberTheory.MulChar.Lemmas
+
 /-!
 # Gauss sums
 
@@ -77,6 +79,20 @@ theorem gaussSum_mulShift (χ : MulChar R R') (ψ : AddChar R R') (a : Rˣ) :
   simp_rw [← mul_assoc, ← map_mul]
   exact Fintype.sum_bijective _ a.mulLeft_bijective _ _ fun x ↦ rfl
 
+/-- Replacing `ψ` by `mulShift ψ a` multiplies the Gauss sum by `χ⁻¹ a`. -/
+theorem gaussSum_mulShift_eq (χ : MulChar R R') (ψ : AddChar R R') (a : Rˣ) :
+    gaussSum χ (ψ.mulShift a) = χ⁻¹ a * gaussSum χ ψ := by
+  rw [← gaussSum_mulShift χ ψ a, inv_apply_eq_inv,
+    Ring.inverse_mul_cancel_left _ _ (a.isUnit.map χ)]
+
+/-- Taking complex conjugates of a Gauss sum inverts both characters. -/
+lemma star_gaussSum_eq (χ : MulChar R ℂ) (ψ : AddChar R ℂ) :
+    star (gaussSum χ ψ) = gaussSum χ⁻¹ ψ⁻¹ :=
+  calc
+    _ = ∑ x, star (ψ x) * χ⁻¹ x := by simp [gaussSum, star_mul, MulChar.star_apply']
+    _ = ∑ x, ψ⁻¹ x * χ⁻¹ x := by simp [← starRingEnd_apply, map_neg_eq_conj]
+    _ = _ := by simp [mul_comm, gaussSum]
+
 end GaussSumDef
 
 /-!