nontrivial_of_nonZeroDivisorsLeft

English

If R is nontrivial and S is contained in the left non-zero divisors, then the localization R[S^{-1}] is nontrivial.

Русский

Если R не тривиально и S содержится в левых делителей нуля, то локализация R[S^{-1}] не тривиальна.

LaTeX

$$(S \le nonZeroDivisorsLeft(R)) ⇒ Nontrivial OreLocalization(S,R)$$

Lean4

theorem nontrivial_of_nonZeroDivisorsLeft [Nontrivial R] (hS : S ≤ nonZeroDivisorsLeft R) : Nontrivial R[S⁻¹] :=
  nontrivial_iff.mpr (fun e ↦ one_ne_zero <| hS e 1 (zero_mul _))

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