mulShift — Mathlib

English

The multiplicative shift of an additive character ψ by r is the character ψ ∘ (x ↦ r x); i.e., (mulShift ψ r)(x) = ψ(r x).

Русский

Умножающий сдвиг аддитивного характера ψ на r задается как композиция ψ с умножением слева на r: (mulShift ψ r)(x) = ψ(r x).

LaTeX

$$$ (mulShift\, \psi\, r)(x) = \psi(r \cdot x)$$$

Lean4

/-- Define the multiplicative shift of an additive character.
This satisfies `mulShift ψ a x = ψ (a * x)`. -/
def mulShift (ψ : AddChar R M) (r : R) : AddChar R M :=
  ψ.compAddMonoidHom (AddMonoidHom.mulLeft r)

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