English
If x and y commute, there exists z in the closure of {x, y} whose order equals the lcm of the orders of x and y.
Русский
Пусть x и y коммутируют; существует z в замыкании множества {x,y}, чьим порядком является НОК порядков x и y.
LaTeX
$$$\\\\exists z \\\\in \\\\mathrm{closure} \\\\{ x, y \}, \\\\operatorname{orderOf} z = \\\\operatorname{lcm}(\\\\operatorname{orderOf} x, \\\\operatorname{orderOf} y)$$$
Lean4
/-- If two commuting elements `x` and `y` of a monoid have order `n` and `m`, then there is an
element of order `lcm n m` that lies in the subgroup generated by `x` and `y`. -/
@[to_additive /-- If two commuting elements `x` and `y` of an additive monoid have order `n` and
`m`, then there is an element of order `lcm n m` that lies in the additive subgroup generated by `x`
and `y`. -/
]
theorem _root_.Commute.exists_orderOf_eq_lcm {x y : G} (h : Commute x y) :
∃ z ∈ closure { x, y }, orderOf z = Nat.lcm (orderOf x) (orderOf y) :=
by
by_cases hx : orderOf x = 0 <;> by_cases hy : orderOf y = 0
· exact ⟨x, subset_closure (by simp), by simp [hx]⟩
· exact ⟨x, subset_closure (by simp), by simp [hx]⟩
· exact ⟨y, subset_closure (by simp), by simp [hy]⟩
·
exact
⟨_, mul_mem (pow_mem (subset_closure (by simp)) _) (pow_mem (subset_closure (by simp)) _),
h.orderOf_mul_pow_eq_lcm hx hy⟩
