zpow_apply

Mathlib.Algebra.Group.AddChar

URI: https://scilib.ai/kg/mathlib#AddChar.zpow_apply

English

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

Русский

Для целого n, аддитивный характер ψ, a ∈ A: (n • ψ)(a) = ψ(a)^n.

LaTeX

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

Lean4

@[simp]
theorem zpow_apply (ψ : AddChar A M) (n : ℤ) (a : A) : (ψ ^ n) a = ψ a ^ n :=
  zsmul_apply ..

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru