prod_eq_top_iff

Mathlib.RingTheory.Ideal.Prod

URI: https://scilib.ai/kg/mathlib#Ideal.prod_eq_top_iff

English

The product I × J is the top ideal iff I and J are both top.

Русский

Произведение I × J равно верхнему идеалу тогда, когда и I, и J верхние.

LaTeX

$$$\\operatorname{prod}(I,J)=\\top \\iff I=\\top \\land J=\\top$$$

Lean4

@[simp]
theorem prod_eq_top_iff {I : Ideal R} {J : Ideal S} : prod I J = ⊤ ↔ I = ⊤ ∧ J = ⊤ := by rw [← prod_inj, prod_top_top]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru