Theorems · Theorem · group theory

Monoid.exponent_prod

∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Monoid M₁] [inst_1 : Monoid M₂],
  Monoid.exponent (M₁ × M₂) = lcm (Monoid.exponent M₁) (Monoid.exponent M₂)

The exponent of product of two monoids is the lcm of the exponents of the individual monoids.

Defined in

Mathlib.GroupTheory.Exponent

Cited by

2 results in Mathlib

Foundations

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

Assumes

MonoidMonoid