instDecompositionMonoidForall — Mathlib

English

If for every i, G i is a decomposition monoid, then the product ∀ i, G i is a decomposition monoid.

Русский

Если для каждого i элемент G_i является декомпозиционным моноидом, то произведение (i → G_i) тоже декомпозиционен.

LaTeX

$$$ [\forall i, DecompositionMonoid (G i)] \Rightarrow DecompositionMonoid (\, (i : ι) → G i \,)$$$

Lean4

instance [∀ i, DecompositionMonoid (G i)] : DecompositionMonoid (∀ i, G i) where
  primal a b c
    h := by
    simp_rw [pi_dvd_iff] at h ⊢
    choose a₁ a₂ h₁ h₂ eq using fun i ↦ DecompositionMonoid.primal _ (h i)
    exact ⟨a₁, a₂, h₁, h₂, funext eq⟩

Похожие утверждения