orderOf_eq — Mathlib

English

In any group G, if a x y form a semiconjugacy h: SemiconjBy a x y, then ord(x) = ord(y).

Русский

В любой группе G, если x и y связаны через полуприведение a x = y a, то ord(x) = ord(y).

LaTeX

$$ \operatorname{order}(x) = \operatorname{order}(y) $$

Lean4

@[to_additive]
theorem orderOf_eq [Group G] (a : G) {x y : G} (h : SemiconjBy a x y) : orderOf x = orderOf y :=
  by
  rw [orderOf_eq_orderOf_iff]
  intro n
  exact (h.pow_right n).eq_one_iff

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