map_nsmul_eq_pow — Mathlib

English

A natural-number multiple maps to a corresponding power: χ(n•x)=χ(x)^n.

Русский

Умножение на натуральное число вносит соответствующую степень: χ(n·x)=χ(x)^n.

LaTeX

$$$\psi(n\,·x)=\psi(x)^n$ for all $n\in\mathbb{N}$ and $x\in A$.$$

Lean4

/-- An additive character maps multiples by natural numbers to powers. -/
theorem map_nsmul_eq_pow (ψ : AddChar A M) (n : ℕ) (x : A) : ψ (n • x) = ψ x ^ n :=
  ψ.toMonoidHom.map_pow x n

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