mem_powers_iff_mem_zpowers — Mathlib

English

The equality of the two representations of powers: powers x and zpowers x are the same as subobjects in a finite group.

Русский

Равенство двух представлений степеней: powers x и zpowers x являются одним и тем же подобъектом в конечной группе.

LaTeX

$$powers x = zpowers x$$

Lean4

@[to_additive]
theorem mem_powers_iff_mem_zpowers : y ∈ powers x ↔ y ∈ zpowers x :=
  (isOfFinOrder_of_finite _).mem_powers_iff_mem_zpowers

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