English
In a NoZeroDivisors setting, the product of two ideals being zero implies one of them is zero: I · J = ⊥ iff I = ⊥ or J = ⊥.
Русский
В кольце без нулевых делителей произведение двух идеалов равно нулю тогда и только тогда, когда один из них равен нулю: I · J = ⊥, если и только если I = ⊥ или J = ⊥.
LaTeX
$$$ \\forall I,J : \\mathrm{Ideal}\\, R,\\ I \\cdot J = \\bot \\iff I = \\bot \\lor J = \\bot$$$
Lean4
@[simp]
theorem mul_eq_bot [NoZeroDivisors R] : I * J = ⊥ ↔ I = ⊥ ∨ J = ⊥ :=
⟨fun hij =>
or_iff_not_imp_left.mpr fun I_ne_bot =>
J.eq_bot_iff.mpr fun j hj =>
let ⟨i, hi, ne0⟩ := I.ne_bot_iff.mp I_ne_bot
Or.resolve_left (mul_eq_zero.mp ((I * J).eq_bot_iff.mp hij _ (mul_mem_mul hi hj))) ne0,
fun h => by obtain rfl | rfl := h; exacts [bot_mul _, mul_bot _]⟩
