QuotientMulEquiv — Mathlib

English

If H and K are complementary with K normal, then the quotient G/K is isomorphic to H.

Русский

Если H и K образуют комплемент, причём K нормальная, то фактор-группа G/K изоморфна H.

LaTeX

$$IsComplement' H K with K.Normal → G/K ≃* H$$

Lean4

/-- If `H` and `K` are complementary with `K` normal, then `G ⧸ K` is isomorphic to `H`. -/
@[simps!]
noncomputable def QuotientMulEquiv [K.Normal] (h : H.IsComplement' K) : G ⧸ K ≃* H :=
  MulEquiv.symm { h.leftQuotientEquiv.symm with map_mul' := fun _ _ ↦ rfl }

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