quotKerEquivRange — Mathlib

English

For a linear map f: M → M2, the quotient M/ker f is linearly isomorphic to the image range f.

Русский

Для линейного отображения f: M → M2 пределы: фактор-модуль M/ker f изоморфен образу f.

LaTeX

$$(M / ker f) ≃ₗ[R] range f$$

Lean4

/-- The **first isomorphism law for modules**. The quotient of `M` by the kernel of `f` is linearly
equivalent to the range of `f`. -/
noncomputable def quotKerEquivRange : (M ⧸ LinearMap.ker f) ≃ₗ[R] LinearMap.range f :=
  (LinearEquiv.ofInjective ((LinearMap.ker f).liftQ f <| le_rfl) <|
        ker_eq_bot.mp <| Submodule.ker_liftQ_eq_bot _ _ _ (le_refl (LinearMap.ker f))).trans
    (LinearEquiv.ofEq _ _ <| Submodule.range_liftQ _ _ _)

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