English
As in gaussSum_aux_of_mulShift, under hd|N, e.mulShift conditions, and unit u, χ(u) gaussSum χ e equals gaussSum χ e, describing invariance of the Gauss sum under a certain unit shift.
Русский
Как и в gaussSum_aux_of_mulShift, при hd|N, условиях e.mulShift и единице u сумма гаусса сохраняет инвариантность: χ(u) gaussSum χ e = gaussSum χ e.
LaTeX
$$$\\text{gaussSum\\_aux\\_of\\_mulShift}(χ,e)\\;: \\; χ(u)\\, gaussSum(χ,e)=gaussSum(χ,e)\\,. $$$
Lean4
theorem gaussSum_aux_of_mulShift (χ : DirichletCharacter R N) {d : ℕ} (hd : d ∣ N) (he : e.mulShift d = 1)
{u : (ZMod N)ˣ} (hu : ZMod.unitsMap hd u = 1) : χ u * gaussSum χ e = gaussSum χ e :=
by
suffices e.mulShift u = e by conv_lhs => rw [← this, gaussSum_mulShift]
rw [(by ring : u.val = (u - 1) + 1), ← mulShift_mul, mulShift_one, mul_eq_right]
rsuffices ⟨a, ha⟩ : (d : ℤ) ∣ (u.val.val - 1 : ℤ)
· have : u.val - 1 = ↑(u.val.val - 1 : ℤ) := by
simp only [ZMod.natCast_val, Int.cast_sub, ZMod.intCast_cast, ZMod.cast_id', id_eq, Int.cast_one]
rw [this, ha]
ext1 y
simpa only [Int.cast_mul, Int.cast_natCast, mulShift_apply, mul_assoc, one_apply] using
DFunLike.ext_iff.mp he (a * y)
rw [← Units.val_inj, Units.val_one, ZMod.unitsMap_def, Units.coe_map] at hu
have : ZMod.castHom hd (ZMod d) u.val = ((u.val.val : ℤ) : ZMod d) := by simp
rwa [MonoidHom.coe_coe, this, ← Int.cast_one, eq_comm, ZMod.intCast_eq_intCast_iff_dvd_sub] at hu
