quotientKerAlgEquivOfSurjective — Mathlib

English

If f: A → B is surjective, then the induced algebra isomorphism A/(ker f) ≃ₐ B exists (quotient Ker map).

Русский

Если f: A → B сюръективен, то существует изоморфизм A/(ker f) ≃ₐ B.

LaTeX

$$$\exists\; (\,A \perp_K \ker f\,) \cong_A B$ for surjective f$$

Lean4

/-- The **first isomorphism theorem** for algebras. -/
@[simps!]
noncomputable def quotientKerAlgEquivOfSurjective {f : A →ₐ[R₁] B} (hf : Function.Surjective f) :
    (A ⧸ (RingHom.ker f)) ≃ₐ[R₁] B :=
  quotientKerAlgEquivOfRightInverse (Classical.choose_spec hf.hasRightInverse)

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