prod — Mathlib

English

The product (cartesian product submonoid) of two finitely generated submonoids is finitely generated.

Русский

Произведение (производное) двух FG-подмонойд FG.

LaTeX

$$FG (P.prod Q)$$

Lean4

/-- The product of two finitely generated submonoids is finitely generated. -/
@[to_additive prod /-- The product of two finitely generated additive submonoids is finitely generated. -/
    ]
theorem prod (hP : P.FG) (hQ : Q.FG) : (P.prod Q).FG := by
  classical
  obtain ⟨bM, hbM⟩ := hP
  obtain ⟨bN, hbN⟩ := hQ
  refine ⟨bM ×ˢ singleton 1 ∪ singleton 1 ×ˢ bN, ?_⟩
  push_cast
  simp [closure_union, hbM, hbN]

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