pow_eq_nsmul

Mathlib.Algebra.Group.AddChar

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

English

For any additive character ψ and n ∈ ℕ, ψ^n = n•ψ.

Русский

Для любого аддитивного характера ψ и натурального n выполняется ψ^n = n•ψ.

LaTeX

$$$\forall \psi: \mathrm{AddChar}(A,M),\forall n\in \mathbb{N},\ \psi^n = n\cdot\psi$$$

Lean4

theorem pow_eq_nsmul (ψ : AddChar A M) (n : ℕ) : ψ ^ n = n • ψ :=
  rfl

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

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

Разделы

Аффилиация

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