coe_zpowers

Mathlib.Algebra.Group.Subgroup.ZPowers.Basic

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

English

The underlying set of zpowers(g) equals { g^n : n ∈ ℤ } when viewed as a subset of G.

Русский

Внутреннее множество zpowers(g) совпадает с { g^n : n ∈ ℤ } как подмножество G.

LaTeX

$$$ \uparrow (zpowers(g)) = \{ g^{n} : n \in \mathbb{Z} \} $$$

Lean4

@[to_additive (attr := norm_cast)] -- TODO: simp?

theorem coe_zpowers (g : G) : ↑(zpowers g) = Set.range (g ^ · : ℤ → G) :=
  rfl

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

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

Разделы

Аффилиация

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