Theorems · Theorem · group theory

AddCommute.addOrderOf_add_nsmul_eq_lcm

∀ {G : Type u} [inst : AddMonoid G] {x y : G},
  AddCommute x y →
    addOrderOf x ≠ 0 →
      addOrderOf y ≠ 0 →
        addOrderOf
            ((addOrderOf x / (addOrderOf x).factorizationLCMLeft (addOrderOf y)) • x +
              (addOrderOf y / (addOrderOf x).factorizationLCMRight (addOrderOf y)) • y) =
          (addOrderOf x).lcm (addOrderOf y)

If two commuting elements x and y of an additive 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 sum of a multiple of x and a multiple of y. See also the result below if you don't need the explicit formula.

Defined in

Mathlib.GroupTheory.Exponent

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddMonoid