map_eq_bot_iff_of_injective — Mathlib

English

If f is injective, then for any ideal I, the image map f I is the bottom ideal iff I is the bottom ideal.

Русский

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

LaTeX

$$$\\forall I\\; (I\\mapsto_f=\\bot) \\iff (I=\\bot)$, assuming $f$ injective.$$

Lean4

theorem map_eq_bot_iff_of_injective {I : Ideal R} {f : F} (hf : Function.Injective f) : I.map f = ⊥ ↔ I = ⊥ := by
  simp [map, span_eq_bot, ← map_zero f, -map_zero, hf.eq_iff, I.eq_bot_iff]

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