primeCompl_le_nonZeroDivisors — Mathlib

English

If P is a prime ideal in a NoZeroDivisors commutative semiring R, then every element not in P is a non-zero-divisor.

Русский

Если P — простой идеал в кольце без делителей нуля, то любой элемент вне P является ненулевым делителем нулей.

LaTeX

$$$\\forall a \\in R,\\ a \\notin P \\Rightarrow a \\in \\operatorname{nonZeroDivisors} R$$$

Lean4

theorem primeCompl_le_nonZeroDivisors {R : Type*} [CommSemiring R] [NoZeroDivisors R] (P : Ideal R) [P.IsPrime] :
    P.primeCompl ≤ nonZeroDivisors R :=
  le_nonZeroDivisors_of_noZeroDivisors <| not_not_intro P.zero_mem

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