infinite_zpowers

Mathlib.Data.ZMod.QuotientGroup

URI: https://scilib.ai/kg/mathlib#infinite_zpowers

English

The z-powers of a are infinite iff a does not have finite order.

Русский

Z-производные a бесконечны тогда и только тогда, когда a не имеет конечного порядка.

LaTeX

$$$ (\mathrm{zpowers}(a)).Infinite \iff \lnot \mathrm{IsOfFinOrder}(a) $$$

Lean4

@[to_additive (attr := simp)]
theorem infinite_zpowers : (zpowers a : Set α).Infinite ↔ ¬IsOfFinOrder a :=
  finite_zpowers.not

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

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

Разделы

Аффилиация

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