English
The exponent of a finite product of monoids equals the least common multiple of the exponents of the factors.
Русский
Экспонента конечного произведения моноидов равна наименьшему общему кратному экспонент составляющих.
LaTeX
$$$\operatorname{exponent}\big(\prod_{i \in ι} M_i\big) = \operatorname{lcm}_{i \in ι} \operatorname{exponent}(M_i)$$$
Lean4
/-- The exponent of finite product of monoids is the `Finset.lcm` of the exponents of the
constituent monoids. -/
@[to_additive /-- The exponent of finite product of additive monoids is the `Finset.lcm` of the
exponents of the constituent additive monoids. -/
]
theorem exponent_pi {ι : Type*} [Fintype ι] {M : ι → Type*} [∀ i, Monoid (M i)] :
exponent ((i : ι) → M i) = lcm univ (exponent <| M ·) :=
by
refine dvd_antisymm ?_ ?_
· refine exponent_dvd_of_forall_pow_eq_one fun m ↦ ?_
ext i
rw [Pi.pow_apply, Pi.one_apply, ← orderOf_dvd_iff_pow_eq_one]
apply dvd_trans (Monoid.order_dvd_exponent (m i))
exact Finset.dvd_lcm (mem_univ i)
· apply Finset.lcm_dvd fun i _ ↦ ?_
exact MonoidHom.exponent_dvd (f := Pi.evalMonoidHom (M ·) i) (Function.surjective_eval i)
