prod_inj — Mathlib

English

The map I, J ↦ I.prod J is injective: if I.prod J = I'.prod J', then I = I' and J = J'.

Русский

Отображение пара (I,J) к I.prod J инъективно: равенство порождает равенство каждого компонента.

LaTeX

$$$\\mathrm{prod}\\,I\\,J = \\mathrm{prod}\\,I'\\,J' \\;\\Rightarrow\\; I = I' \\text{ и } J = J'$$$

Lean4

@[simp]
theorem prod_inj {I I' : Ideal R} {J J' : Ideal S} : prod I J = prod I' J' ↔ I = I' ∧ J = J' := by
  simp only [← idealProdEquiv_symm_apply, idealProdEquiv.symm.injective.eq_iff, Prod.mk_inj]

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