English
Let A be an additive group and M a commutative monoid. For any additive character ψ: A → M and any natural number n, the nth power ψ^n, regarded as a function, corresponds to the pointwise n-th power: (ψ^n)(a) = (ψ(a))^n for all a ∈ A.
Русский
Пусть A — аддитивная группа, M — коммутативный моноид. Для любого аддитивного характера ψ: A → M и любого натурального числа n тождествено выполняется: ψ^n, рассматриваемый как функция, равен по значению функции n-й степенью: (ψ^n)(a) = (ψ(a))^n для всех a ∈ A.
LaTeX
$$$\forall \psi: \mathrm{AddChar}(A,M)\ \forall n \in \mathbb{N},\ (\psi^n)(a) = (\psi(a))^n \quad (\text{for all } a\in A).$$$
Lean4
@[simp, norm_cast]
theorem coe_pow (ψ : AddChar A M) (n : ℕ) : ⇑(ψ ^ n) = ψ ^ n :=
rfl
