prod — Mathlib

English

The product of two finitely generated subgroups is finitely generated.

Русский

Произведение двух конечнопорожденных подгрупп FG.

LaTeX

$$$\forall {G : Type*} [Group G] {P : Subgroup G} {Q : Subgroup G}, P.FG \to Q.FG \to (P.prod Q).FG$$$

Lean4

/-- The product of two finitely generated subgroups is finitely generated. -/
@[to_additive prod /-- The product of two finitely generated additive subgroups is finitely generated. -/
    ]
theorem prod {G' : Type*} [Group G'] {P : Subgroup G} {Q : Subgroup G'} (hP : P.FG) (hQ : Q.FG) : (P.prod Q).FG :=
  by
  rw [fg_iff_submonoid_fg] at *
  exact hP.prod hQ

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