mulShift_mul — Mathlib

English

Let ψ be an additive character from R to M. Then for all r, s in R, mulShift ψ r · mulShift ψ s = mulShift ψ (r + s).

Русский

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

LaTeX

$$$mulShift(ψ, r) · mulShift(ψ, s) = mulShift(ψ, r+s)$$$

Lean4

/-- The product of `mulShift ψ r` and `mulShift ψ s` is `mulShift ψ (r + s)`. -/
theorem mulShift_mul (ψ : AddChar R M) (r s : R) : mulShift ψ r * mulShift ψ s = mulShift ψ (r + s) :=
  by
  ext
  rw [mulShift_apply, right_distrib, map_add_eq_mul]; norm_cast

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