map_eq_bot_iff_le_ker — Mathlib

English

For a map f of a ring-like structure, the image of I under f is the bottom ideal iff I is contained in the kernel of f.

Русский

Изображение идеала I под отображением f равно нулю тогда и только тогда, когда I ⊆ ker f.

LaTeX

$$$ I.map f = \\bot \\iff I \\le \\ker f. $$$

Lean4

theorem map_eq_bot_iff_le_ker {I : Ideal R} (f : F) : I.map f = ⊥ ↔ I ≤ RingHom.ker f := by
  rw [RingHom.ker, eq_bot_iff, map_le_iff_le_comap]

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