mulShift_mulShift — Mathlib

English

For ψ an additive character, and r, s ∈ R, mulShift (mulShift ψ r) s = mulShift ψ (r * s).

Русский

Пусть ψ — аддитивный характер; для любых r, s ∈ R выполняется: mulShift (mulShift ψ r) s = mulShift ψ (r · s).

LaTeX

$$$mulShift(mulShift(ψ, r), s) = mulShift(ψ, r * s)$$$

Lean4

theorem mulShift_mulShift (ψ : AddChar R M) (r s : R) : mulShift (mulShift ψ r) s = mulShift ψ (r * s) :=
  by
  ext
  simp only [mulShift_apply, mul_assoc]

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