mulEquivSubgroup — Mathlib

English

A sequence of lemmas showing that the map between the subgroup semidirect product and G is bijective under the given complement condition.

Русский

Серия лемм, доказывающих биективность отображения между подпроизведением-сепаратором и G при заданном условии дополнения.

LaTeX

$$$ \text{MulEquiv}(H \rtimes[... ] K, G) \;\text{bijective} $$$

Lean4

/-- The isomorphism from a semidirect product of complementary subgroups to the ambient group. -/
@[simps!]
noncomputable def mulEquivSubgroup {H K : Subgroup G} [H.Normal] (h : H.IsComplement' K) :
    H ⋊[(H.normalizerMonoidHom).comp (inclusion (H.normalizer_eq_top ▸ le_top))] K ≃* G :=
  MulEquiv.ofBijective (monoidHomSubgroup _) ((equivProd.bijective_comp _).mpr h)

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