powers_eq_zpowers

Mathlib.GroupTheory.OrderOfElement

URI: https://scilib.ai/kg/mathlib#IsOfFinOrder.powers_eq_zpowers

English

For IsOfFinOrder x, the set of powers of x equals the set of zpowers of x.

Русский

Для IsOfFinOrder x множество степеней x совпадает с множеством z-пуктов x.

LaTeX

$$powers x = zpowers x$$

Lean4

@[to_additive]
theorem powers_eq_zpowers (hx : IsOfFinOrder x) : (powers x : Set G) = zpowers x :=
  Set.ext fun _ ↦ hx.mem_powers_iff_mem_zpowers

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

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

Разделы

Аффилиация

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