English
If a direct product has finite order then so does each component.
Русский
Если произведение имеет конечный порядок, то и каждый компонент имеет конечный порядок.
LaTeX
$$IsOfFinOrder x \\Rightarrow \\forall i, IsOfFinOrder (x i)$$
Lean4
/-- If a direct product has finite order then so does each component. -/
@[to_additive /-- If a direct product has finite additive order then so does each component. -/
]
theorem apply {η : Type*} {Gs : η → Type*} [∀ i, Monoid (Gs i)] {x : ∀ i, Gs i} (h : IsOfFinOrder x) :
∀ i, IsOfFinOrder (x i) := by
obtain ⟨n, npos, hn⟩ := h.exists_pow_eq_one
exact fun _ => isOfFinOrder_iff_pow_eq_one.mpr ⟨n, npos, (congr_fun hn.symm _).symm⟩
