zpow_mem_zpowers

Mathlib.Algebra.Group.Subgroup.ZPowers.Basic

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

English

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

Русский

Для каждого g ∈ G и каждого целого k,m принадлежит g^k циклической подпгруппе zpowers(g).

LaTeX

$$$ g^k \in \operatorname{zpowers}(g) $$$

Lean4

@[to_additive (attr := simp)]
theorem zpow_mem_zpowers (g : G) (k : ℤ) : g ^ k ∈ zpowers g :=
  mem_zpowers_iff.mpr ⟨k, rfl⟩

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

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

Разделы

Аффилиация

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