nontrivial_of_nonZeroDivisorsRight

English

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

Русский

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

LaTeX

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

Lean4

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

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