npow_mem_zpowers

Mathlib.Algebra.Group.Subgroup.ZPowers.Basic

URI: https://scilib.ai/kg/mathlib#Subgroup.npow_mem_zpowers

English

For every g ∈ G and every k ∈ ℕ, g^k ∈ zpowers(g).

Русский

Для каждого g ∈ G и каждого k ∈ ℕ, g^k ∈ zpowers(g).

LaTeX

$$$ g^k \in \operatorname{zpowers}(g) \quad\text{for all } k \in \mathbb N$$$

Lean4

@[to_additive (attr := simp)]
theorem npow_mem_zpowers (g : G) (k : ℕ) : g ^ k ∈ zpowers g :=
  zpow_natCast g k ▸ zpow_mem_zpowers g k

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

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

Разделы

Аффилиация

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