quotKerEquivOfSurjective — Mathlib

English

If f is surjective, then M/ker f ≃ M2.

Русский

Если линейное отображение f сюръективно, то фактор-пространство M/ker f изоморфно M2.

LaTeX

$$(M / ker f) ≃ₗ[R] M₂, при hf: Function.Surjective f$$

Lean4

/-- The **first isomorphism theorem for surjective linear maps**. -/
noncomputable def quotKerEquivOfSurjective (f : M →ₗ[R] M₂) (hf : Function.Surjective f) :
    (M ⧸ LinearMap.ker f) ≃ₗ[R] M₂ :=
  f.quotKerEquivRange.trans <| .ofTop (LinearMap.range f) <| range_eq_top.2 hf

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