powers_eq_zpowers

Mathlib.GroupTheory.OrderOfElement

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

English

Definition of the equivalence between zpowers and powers via finiteness and order.

Русский

Определение эквивалентности между zpowers и powers через конечность и порядок.

LaTeX

$$zpowersEquivZPowers : Eq (orderOf x) (orderOf y) → Equiv (zpowers x) (zpowers y)$$

Lean4

@[to_additive]
theorem powers_eq_zpowers (x : G) : (powers x : Set G) = zpowers x :=
  (isOfFinOrder_of_finite _).powers_eq_zpowers

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

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

Разделы

Аффилиация

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