disjoint_nonZeroDivisors_of_mem_minimalPrimes

English

For p ∈ minimalPrimes R, p is disjoint from the set of non-zero divisors of R.

Русский

Для p ∈ minimalPrimes R, множество p и множество ненулевых делителей R непересекаются.

LaTeX

$$$\forall p \in minimalPrimes(R),\; (p : Set\,R) \perp (nonZeroDivisors\,R)$$$

Lean4

/-- minimal primes are contained in zero divisors. -/
theorem disjoint_nonZeroDivisors_of_mem_minimalPrimes {p : Ideal R} (hp : p ∈ minimalPrimes R) :
    Disjoint (p : Set R) (nonZeroDivisors R) :=
  by
  simp_rw [Set.disjoint_left, SetLike.mem_coe, mem_nonZeroDivisors_iff_right, not_forall, exists_prop,
    @and_comm (_ * _ = _), ← mul_comm]
  exact fun _ ↦ Ideal.exists_mul_mem_of_mem_minimalPrimes hp

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