English
The product of two Lie groups carries a natural Lie group structure, with product and inverse defined componentwise.
Русский
Произведение двух Lie-групп естественно обладает структурой Lie-группы с покомпонентным умножением и обращением.
LaTeX
$$LieGroup (I.prod I') n (G × G') with ContMDiffMul.prod and contMDiff_inv = contMDiff_fst.inv.prodMk contMDDiff_snd.inv$$
Lean4
@[to_additive]
instance instLieGroup {𝕜 : Type*} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type*} [TopologicalSpace H]
{E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type*} [TopologicalSpace G]
[ChartedSpace H G] [Group G] [LieGroup I n G] {E' : Type*} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type*}
[TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {G' : Type*} [TopologicalSpace G'] [ChartedSpace H' G']
[Group G'] [LieGroup I' n G'] : LieGroup (I.prod I') n (G × G') :=
{ ContMDiffMul.prod _ _ _ _ with contMDiff_inv := contMDiff_fst.inv.prodMk contMDiff_snd.inv }
