jacobiSum_comm — Mathlib

English

For multiplicative characters χ and ψ, the Jacobi sum is symmetric: J(χ, ψ) = J(ψ, χ).

Русский

Для мультипликативных символов χ и ψ сумма Якоби симметрична: J(χ, ψ) = J(ψ, χ).

LaTeX

$$$$ J(\chi, \psi) = J(\psi, \chi). $$$$

Lean4

theorem jacobiSum_comm (χ ψ : MulChar R R') : jacobiSum χ ψ = jacobiSum ψ χ :=
  by
  simp only [jacobiSum, mul_comm (χ _)]
  rw [← (Equiv.subLeft 1).sum_comp]
  simp only [Equiv.subLeft_apply, sub_sub_cancel]

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