English
For subgroups H ≤ G and K ≤ N, the product H × K forms a subgroup of G × N; namely, the direct product of subgroups is a subgroup of the direct product group.
Русский
Пусть H ⊆ G и K ⊆ N — подгруппы. Их прямое произведение H × K образует подгруппу в G × N, то есть параллельное произведение образует подгруппу.
LaTeX
$$$ H \\times K \\le G \\times N $ and $ (H, K) \\mapsto H \\times K $ is a subgroup of $G \\times N$$$
Lean4
/-- Given `Subgroup`s `H`, `K` of groups `G`, `N` respectively, `H × K` as a subgroup of `G × N`. -/
@[to_additive prod /-- Given `AddSubgroup`s `H`, `K` of `AddGroup`s `A`, `B` respectively, `H × K`
as an `AddSubgroup` of `A × B`. -/
]
def prod (H : Subgroup G) (K : Subgroup N) : Subgroup (G × N) :=
{ Submonoid.prod H.toSubmonoid K.toSubmonoid with inv_mem' := fun hx => ⟨H.inv_mem' hx.1, K.inv_mem' hx.2⟩ }
