Theorems · Theorem · group theory

Commute.orderOf_mul_pow_eq_lcm

∀ {G : Type u} [inst : Monoid G] {x y : G},
  Commute x y →
    orderOf x ≠ 0 →
      orderOf y ≠ 0 →
        orderOf
            (x ^ (orderOf x / (orderOf x).factorizationLCMLeft (orderOf y)) *
              y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y))) =
          (orderOf x).lcm (orderOf y)

If two commuting elements x and y of a monoid have order n and m, there is an element of order lcm n m. The result actually gives an explicit (computable) element, written as the product of a power of x and a power of y. See also the result below if you don't need the explicit formula.

Defined in

Mathlib.GroupTheory.Exponent

Cited by

2 results in Mathlib

Foundations

Depth 100 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Monoid