map_zsmul_eq_zpow — Mathlib

English

For additive character ψ and integer n, and a ∈ A, ψ(n • a) = (ψ(a))^n.

Русский

Пусть ψ — аддитивный характер, n целое, a ∈ A. Тогда ψ(n • a) = (ψ(a))^n.

LaTeX

$$$\forall n \in \mathbb{Z},\forall a\in A,\ ψ(n\cdot a) = (ψ(a))^{n}.$$$

Lean4

/-- An additive character maps integer scalar multiples to integer powers. -/
theorem map_zsmul_eq_zpow (ψ : AddChar A M) (n : ℤ) (a : A) : ψ (n • a) = (ψ a) ^ n :=
  ψ.toMonoidHom.map_zpow a n

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