instNoZeroDivisors — Mathlib

English

If the base ring R has no zero divisors, then the ideal ring inherits this property: for any ideals I,J, I · J = ⊥ implies I = ⊥ or J = ⊥.

Русский

Если базовое кольцо R не имеет нулевых делителей, то кольцо идеалов наследует это свойство: для любых идеалов I,J выполняется I · J = ⊥ => I = ⊥ или J = ⊥.

LaTeX

$$$ \\forall I,J : \\mathrm{Ideal}\\, R,\\ I \\cdot J = \\bot \\Rightarrow I = \\bot \\lor J = \\bot$$$

Lean4

instance [NoZeroDivisors R] : NoZeroDivisors (Ideal R) where eq_zero_or_eq_zero_of_mul_eq_zero := mul_eq_bot.1

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