quotientRangeInlEquivRight — Mathlib

English

There is an isomorphism E / S.inl.range ≅* G induced by the rightHom, composing with the range of S.inl.

Русский

Существует изоморфизм E / S.inl.range ≅* G, индуцированный rightHom и диапазон S.inl.

LaTeX

$$$ E \\;/ S.inl.range \\cong* G $$$

Lean4

/-- The isomorphism `E ⧸ S.inl.range ≃* G` induced by `S.rightHom` -/
@[to_additive /-- The isomorphism `E ⧸ S.inl.range ≃+ G` induced by `S.rightHom` -/
    ]
noncomputable def quotientRangeInlEquivRight : E ⧸ S.inl.range ≃* G :=
  (QuotientGroup.quotientMulEquivOfEq S.range_inl_eq_ker_rightHom).trans S.quotientKerRightHomEquivRight

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