mk_ker — Mathlib

English

Let I be a two‑sided ideal in a ring R. The kernel of the quotient map π_I: R → R/I is exactly I.

Русский

Пусть I — двусторонний идеал кольца R. Ядро гомоморфизма тождества $R \to R/I$ по факторизации равно I.

LaTeX

$$$\ker(\operatorname{Quotient.mk} I) = I$$$

Lean4

@[simp]
theorem mk_ker {I : Ideal R} [I.IsTwoSided] : ker (Quotient.mk I) = I :=
  by
  ext
  rw [ker, mem_comap, Submodule.mem_bot, Quotient.eq_zero_iff_mem]

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