instDecompositionMonoidProd — Mathlib

English

If G1 and G2 are decomposition monoids, then their product G1 × G2 is a decomposition monoid.

Русский

Если G1 и G2 — декомпозиционные моноиды, то их произведение G1 × G2 тоже является декомпозиционным моноидом.

LaTeX

$$$ [DecompositionMonoid\; G_1] \;[DecompositionMonoid\; G_2] \Rightarrow DecompositionMonoid (G_1 \times G_2)$$$

Lean4

instance [DecompositionMonoid G₁] [DecompositionMonoid G₂] : DecompositionMonoid (G₁ × G₂) where
  primal a b c
    h := by
    simp_rw [prod_dvd_iff] at h ⊢
    obtain ⟨a₁, a₁', h₁, h₁', eq₁⟩ := DecompositionMonoid.primal a.1 h.1
    obtain ⟨a₂, a₂', h₂, h₂', eq₂⟩ :=
      DecompositionMonoid.primal a.2
        h.2
          -- aesop works here

    exact ⟨(a₁, a₂), (a₁', a₂'), ⟨h₁, h₂⟩, ⟨h₁', h₂'⟩, Prod.ext eq₁ eq₂⟩

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