map_snd_prod — Mathlib

English

The image of the product ideal I × J under the projection snd is precisely J.

Русский

Образ произведения идеалов I и J по проекции snd равен J.

LaTeX

$$$\\operatorname{map} (\\text{snd}) (I \\mathrm{prod} J) = J$$$

Lean4

@[simp]
theorem map_snd_prod (I : Ideal R) (J : Ideal S) : map (RingHom.snd R S) (prod I J) = J :=
  by
  ext x
  rw [mem_map_iff_of_surjective (RingHom.snd R S) Prod.snd_surjective]
  exact
    ⟨by
      rintro ⟨x, ⟨h, rfl⟩⟩
      exact h.2, fun h => ⟨⟨0, x⟩, ⟨⟨Ideal.zero_mem _, h⟩, rfl⟩⟩⟩

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