jacobiSum_ringHomComp — Mathlib

English

Jacobi sums are compatible with ring homomorphisms: J(χ ∘ f, ψ ∘ f) = f(J(χ, ψ)).

Русский

Суммы Якоби совместимы с кольцевыми гомоморфизмами: J(χ ∘ f, ψ ∘ f) = f(J(χ, ψ)).

LaTeX

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

Lean4

/-- The Jacobi sum is compatible with ring homomorphisms. -/
theorem jacobiSum_ringHomComp {R'' : Type*} [CommRing R''] (χ ψ : MulChar R R') (f : R' →+* R'') :
    jacobiSum (χ.ringHomComp f) (ψ.ringHomComp f) = f (jacobiSum χ ψ) := by
  simp only [jacobiSum, MulChar.ringHomComp, MulChar.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk, map_sum, map_mul]

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