ker_ringCon_mk' — Mathlib

English

The kernel of the canonical quotient map R → R/I is exactly I.

Русский

Ядро канонического отображения R → R/I равно I.

LaTeX

$$$\\ker(I.ringCon.mk') = I$$$

Lean4

/-- The kernel of the ring homomorphism `R → R⧸I` is `I`.
-/
@[simp]
theorem ker_ringCon_mk' (I : TwoSidedIdeal R) : ker I.ringCon.mk' = I :=
  le_antisymm (fun _ h => by simpa using I.rel_iff _ _ |>.1 (Quotient.eq'.1 h))
    (fun _ h => Quotient.sound' <| I.rel_iff _ _ |>.2 (by simpa using h))

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