English
Let H ≤ G and K ≤ N be subgroups. The product subgroup H × K in G × N has as its underlying set the cartesian product H × K; that is, (H.prod K : Set (G × N)) = (H : Set G) × (K : Set N).
Русский
Пусть H — подгруппа G и K — подгруппа N. Произведение подгрупп H × K внутри G × N имеет множество подлежащих элементов, равное декартовому произведению H × K: (H.prod K : Set (G × N)) = (H : Set G) × (K : Set N).
LaTeX
$$$ (H \times K : \mathrm{Set}(G \times N)) = (H : \mathrm{Set} G) \times (K : \mathrm{Set} N) $$$
Lean4
@[to_additive (attr := norm_cast) coe_prod]
theorem coe_prod (H : Subgroup G) (K : Subgroup N) : (H.prod K : Set (G × N)) = (H : Set G) ×ˢ (K : Set N) :=
rfl
