English
The exponent of a product of two monoids equals the lcm of the exponents of the two factors.
Русский
Экспонента произведения двух моноидов равна наименьшему общему кратному экспонент двух факторов.
LaTeX
$$$\operatorname{exponent}(M_1 \times M_2) = \operatorname{lcm}(\operatorname{exponent}(M_1), \operatorname{exponent}(M_2))$$$
Lean4
/-- The exponent of product of two monoids is the `lcm` of the exponents of the
individual monoids. -/
@[to_additive AddMonoid.exponent_prod /-- The exponent of product of two additive monoids is the
`lcm` of the exponents of the individual additive monoids. -/
]
theorem exponent_prod {M₁ M₂ : Type*} [Monoid M₁] [Monoid M₂] : exponent (M₁ × M₂) = lcm (exponent M₁) (exponent M₂) :=
by
refine dvd_antisymm ?_ (lcm_dvd ?_ ?_)
· refine exponent_dvd_of_forall_pow_eq_one fun g ↦ ?_
ext1
· rw [Prod.pow_fst, Prod.fst_one, ← orderOf_dvd_iff_pow_eq_one]
exact dvd_trans (Monoid.order_dvd_exponent (g.1)) <| dvd_lcm_left _ _
· rw [Prod.pow_snd, Prod.snd_one, ← orderOf_dvd_iff_pow_eq_one]
exact dvd_trans (Monoid.order_dvd_exponent (g.2)) <| dvd_lcm_right _ _
· exact MonoidHom.exponent_dvd (f := MonoidHom.fst M₁ M₂) Prod.fst_surjective
· exact MonoidHom.exponent_dvd (f := MonoidHom.snd M₁ M₂) Prod.snd_surjective
