mkₐ_ker — Mathlib

English

Let I be a two-sided ideal of A. The kernel of the canonical ring homomorphism (A →ₐ[R1] A/I) given by Quotient.mk I is precisely I.

Русский

Пусть I — двусторонний идеал A. Ядро канонического кольцевого отображения A → A/I по mk I совпадает с I.

LaTeX

$$$\mathrm{ker}\bigl( \operatorname{Quotient.mk}_I : A \to A/I \bigr) = I$$$

Lean4

/-- The kernel of `A →ₐ[R₁] I.quotient` is `I`. -/
@[simp]
theorem mkₐ_ker (I : Ideal A) [I.IsTwoSided] : RingHom.ker (Quotient.mkₐ R₁ I : A →+* A ⧸ I) = I :=
  Ideal.mk_ker

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