Theorems · Theorem · group theory

Commute.orderOf_mul_eq_right_of_forall_prime_mul_dvd

∀ {G : Type u_1} [inst : Monoid G] {x y : G},
  Commute x y →
    IsOfFinOrder y → (∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y) → orderOf (x * y) = orderOf y

If each prime factor of orderOf x has higher multiplicity in orderOf y, and x commutes with y, then x * y has the same order as y.

Defined in

Mathlib.GroupTheory.OrderOfElement

Cited by

2 results in Mathlib

Foundations

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

Assumes

Monoid