coe_nsmul — Mathlib

English

Let n be a natural number and ψ an additive character. Then the function underlying n•ψ (n-fold addition of ψ) is the nth power of ψ: (n • ψ)(a) = (ψ(a))^n for all a ∈ A.

Русский

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

LaTeX

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

Lean4

@[simp, norm_cast]
theorem coe_nsmul (n : ℕ) (ψ : AddChar A M) : ⇑(n • ψ) = ψ ^ n :=
  rfl

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