isDomain_of_atPrime — Mathlib

English

Under IsLocalization.AtPrime, the ring S is a domain.

Русский

При условии IsLocalization.AtPrime кольцо S является доменом.

LaTeX

$$$$ \text{IsDomain } S $$$$

Lean4

/-- This is an `IsLocalization.AtPrime` version for `IsLocalization.isDomain_of_local_atPrime`. -/
theorem isDomain_of_atPrime (S : Type*) [CommSemiring S] [Algebra A S] (P : Ideal A) [P.IsPrime]
    [IsLocalization.AtPrime S P] : IsDomain S :=
  isDomain_of_le_nonZeroDivisors S P.primeCompl_le_nonZeroDivisors

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