quotientKerEquivRange — Mathlib

Lean4
/-- The **first isomorphism theorem for monoids**. -/
@[to_additive /-- The first isomorphism theorem for `AddMonoid`s. -/
    ]
noncomputable def quotientKerEquivRange (f : M →* P) : (ker f).Quotient ≃* MonoidHom.mrange f :=
  {
    Equiv.ofBijective
        ((@MulEquiv.toMonoidHom (MonoidHom.mrange (kerLift f)) _ _ _ <| MulEquiv.submonoidCongr kerLift_range_eq).comp
          (kerLift f).mrangeRestrict) <|
      ((Equiv.bijective
            (@MulEquiv.toEquiv (MonoidHom.mrange (kerLift f)) _ _ _ <| MulEquiv.submonoidCongr kerLift_range_eq)).comp
        ⟨fun x y h => kerLift_injective f <| by rcases x with ⟨⟩; rcases y with ⟨⟩; injections, fun ⟨w, z, hz⟩ =>
          ⟨z, by rcases hz with ⟨⟩; rfl⟩⟩) with
    map_mul' := MonoidHom.map_mul _ }
Похожие утверждения