Theorems · Theorem · group theory

AddCommute.addOrderOf_add_eq_right_of_forall_prime_mul_dvd

∀ {G : Type u_1} [inst : AddMonoid G] {x y : G},
  AddCommute x y →
    IsOfFinAddOrder y →
      (∀ (p : ℕ), Nat.Prime p → p ∣ addOrderOf x → p * addOrderOf x ∣ addOrderOf y) → addOrderOf (x + y) = addOrderOf y

If each prime factor of addOrderOf x has higher multiplicity in addOrderOf 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

AddMonoid