mul_gaussSum_inv_eq_gaussSum — Mathlib

English

For χ, ψ, gaussSum χ ψ⁻¹ multiplied by χ(−1) equals gaussSum χ ψ.

Русский

Для χ, ψ гауссова сумма χ ψ⁻¹, умноженная на χ(−1), равна gaussSum χ ψ.

LaTeX

$$$\chi(-1) \cdot \mathrm{gaussSum}(\chi, ψ^{-1}) = \mathrm{gaussSum}(\chi, ψ)$$$

Lean4

theorem mul_gaussSum_inv_eq_gaussSum (χ : MulChar R R') (ψ : AddChar R R') : χ (-1) * gaussSum χ ψ⁻¹ = gaussSum χ ψ :=
  by
  rw [ψ.inv_mulShift, ← Units.coe_neg_one]
  exact gaussSum_mulShift χ ψ (-1)

Похожие утверждения