quotientKerEquivOfSurjective — Mathlib

English

If f is surjective, then the quotient by the kernel is isomorphic to S via quotientKerEquivOfSurjective.

Русский

Если отображение сюръективно, то R/ker f изоморфно S через QuotientKerEquivOfSurjective.

LaTeX

$$$$R/\ker f \cong+* S \quad\text{when } f\ \text{is surjective}.$$$$

Lean4

/-- The **first isomorphism theorem** for commutative rings, surjective case. -/
noncomputable def quotientKerEquivOfSurjective (hf : Function.Surjective f) : R ⧸ (ker f) ≃+* S :=
  quotientKerEquivOfRightInverse (Classical.choose_spec hf.hasRightInverse)

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