toSubgroup_prod — Mathlib

English

For open subgroups U ≤ G and V ≤ H, the subgroup of G × H generated by their product coincides with the external direct product of the two subgroups, i.e., (U.prod V) = (U : Subgroup G) .prod V.

Русский

Пусть U ≤ G и V ≤ H — открытые подгруппы. Подгруппа G × H, порожденная их произведением, совпадает с внешним прямым произведением двух подгрупп: (U.prod V) = (U : Subgroup G).prod V.

LaTeX

$$$$(U \\mathrm{prod} V) = (U \\mathrm{asSubgroup}) \\mathrm{prod} V.$$$$

Lean4

@[to_additive (attr := simp, norm_cast) toAddSubgroup_prod]
theorem toSubgroup_prod (U : OpenSubgroup G) (V : OpenSubgroup H) :
    (U.prod V : Subgroup (G × H)) = (U : Subgroup G).prod V :=
  rfl

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