theorem nontrivial_localization_iff_le_nonZeroDivisors {R : Type u_1} [CommRing R] [IsDomain R] {s : Submonoid R} : Nontrivial (Localization s) ↔ s ≤ nonZeroDivisors R

theorem le_nonZeroDivisors_of_nontrivial_localization {R : Type u_1} [CommRing R] [IsDomain R] (s : Submonoid R) [i : Nontrivial (Localization s)] : s ≤ nonZeroDivisors R

theorem Localization.coe_denom_ne_zero {R : Type u_1} [CommRing R] {s : Submonoid R} [Nontrivial (Localization s)] (a : ↥s) : ↑a ≠ 0

theorem Localization.r_iff_of_nontrivial {R : Type u_1} [CommRing R] [IsDomain R] {s : Submonoid R} [Nontrivial (Localization s)] (a c : R) (b d : ↥s) : (r s) (a, b) (c, d) ↔ a * ↑d = ↑b * c

@[reducible]

def Localization.nonneg_priv {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (s : Submonoid R) [Nontrivial (Localization s)] : Subsemiring (Localization s)

Equations

• Localization.nonneg_priv s = { carrier := {x : Localization s | x.liftOn (fun (a₁ : R) (a₂ : ↥s) => 0 ≤ a₁ * ↑a₂) ⋯}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯ }

theorem Localization.isPointed_nonneg_priv {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (s : Submonoid R) [Nontrivial (Localization s)] : (nonneg_priv s).toAddSubmonoid.IsPointed

@[instance_reducible]

instance Localization.instDecidablePredMemAddSubmonoidToAddSubmonoidNonneg_priv {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (s : Submonoid R) [Nontrivial (Localization s)] : DecidablePred fun (x : Localization s) => x ∈ (nonneg_priv s).toAddSubmonoid

Equations

• Localization.instDecidablePredMemAddSubmonoidToAddSubmonoidNonneg_priv s x = x.recOnSubsingleton fun (a₁ : R) (a₂ : ↥s) => decidable_of_iff' (0 ≤ a₁ * ↑a₂) ⋯

@[instance_reducible]

instance Localization.instLinearOrder_realClosedField {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (s : Submonoid R) [Nontrivial (Localization s)] : LinearOrder (Localization s)

Equations

• Localization.instLinearOrder_realClosedField s = LinearOrder.ofAddSubmonoid ⋯ ⋯

instance Localization.instIsOrderedRing_realClosedField {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (s : Submonoid R) [Nontrivial (Localization s)] : IsOrderedRing (Localization s)

@[simp]

theorem Localization.mk_le_mk₀ {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (s : Submonoid R) [Nontrivial (Localization s)] (a₁ b₁ : R) (a₂ b₂ : ↥s) : mk a₁ a₂ ≤ mk b₁ b₂ ↔ a₁ * ↑a₂ * ↑b₂ * ↑b₂ ≤ b₁ * ↑b₂ * ↑a₂ * ↑a₂

@[simp]

theorem Localization.algebraMap_mono {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (s : Submonoid R) [Nontrivial (Localization s)] (a b : R) : (algebraMap R (Localization s)) a ≤ (algebraMap R (Localization s)) b ↔ a ≤ b

theorem Localization.algebraMap_monotone {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (s : Submonoid R) [Nontrivial (Localization s)] : Monotone ⇑(algebraMap R (Localization s))