mathlib3 documentation

ring_theory.ore_localization.basic

Localization over right Ore sets. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines the localization of a monoid over a right Ore set and proves its universal mapping property. It then extends the definition and its properties first to semirings and then to rings. We show that in the case of a commutative monoid this definition coincides with the common monoid localization. Finally we show that in a ring without zero divisors, taking the Ore localization at R - {0} results in a division ring.

Notations #

Introduces the notation R[S⁻¹] for the Ore localization of a monoid R at a right Ore subset S. Also defines a new heterogeneos division notation r /ₒ s for a numerator r : R and a denominator s : S.

References #

Tags #

localization, Ore, non-commutative

source
def ore_localization.ore_eqv (R : Type u_1) [monoid R] (S : submonoid R) [ore_localization.ore_set S] :
setoid (R × ↥S)

The setoid on R × S used for the Ore localization.

Equations
source
def ore_localization (R : Type u_1) [monoid R] (S : submonoid R) [ore_localization.ore_set S] :
Type u_1

The ore localization of a monoid and a submonoid fulfilling the ore condition.

Equations
Instances for ore_localization
source
def ore_localization.ore_div {R : Type u_1} [monoid R] {S : submonoid R} [ore_localization.ore_set S] (r : R) (s : ↥S) :
R[S⁻¹]

The division in the ore localization R[S⁻¹], as a fraction of an element of R and S.

Equations
source
@[protected]
theorem ore_localization.ind {R : Type u_1} [monoid R] {S : submonoid R} [ore_localization.ore_set S] {β : R[S⁻¹] → Prop} (c : ∀ (r : R) (s : ↥S), β (r /ₒ s)) (q : R[S⁻¹]) :
β q
source
theorem ore_localization.ore_div_eq_iff {R : Type u_1} [monoid R] {S : submonoid R} [ore_localization.ore_set S] {r₁ r₂ : R} {s₁ s₂ : ↥S} :
r₁ /ₒ s₁ = r₂ /ₒ s₂ ↔ ∃ (u : ↥S) (v : R), r₂ * ↑u = r₁ * v ∧ ↑s₂ * ↑u = ↑s₁ * v
source
@[protected]
theorem ore_localization.expand {R : Type u_1} [monoid R] {S : submonoid R} [ore_localization.ore_set S] (r : R) (s : ↥S) (t : R) (hst : ↑s * t ∈ S) :
r /ₒ s = r * t /ₒ ⟨↑s * t, hst⟩

A fraction r /ₒ s is equal to its expansion by an arbitrary factor t if s * t ∈ S.

source
@[protected]
theorem ore_localization.expand' {R : Type u_1} [monoid R] {S : submonoid R} [ore_localization.ore_set S] (r : R) (s s' : ↥S) :
r /ₒ s = r * ↑s' /ₒ (s * s')

A fraction is equal to its expansion by an factor from s.

source
@[protected]
theorem ore_localization.eq_of_num_factor_eq {R : Type u_1} [monoid R] {S : submonoid R} [ore_localization.ore_set S] {r r' r₁ r₂ : R} {s t : ↥S} (h : r * ↑t = r' * ↑t) :
r₁ * r * r₂ /ₒ s = r₁ * r' * r₂ /ₒ s

Fractions which differ by a factor of the numerator can be proven equal if those factors expand to equal elements of R.

source
def ore_localization.lift_expand {R : Type u_1} [monoid R] {S : submonoid R} [ore_localization.ore_set S] {C : Sort u_2} (P : R → ↥S → C) (hP : ∀ (r t : R) (s : ↥S) (ht : ↑s * t ∈ S), P r s = P (r * t) ⟨↑s * t, ht⟩) :
R[S⁻¹] → C

A function or predicate over R and S can be lifted to R[S⁻¹] if it is invariant under expansion on the right.

Equations
source
@[simp]
theorem ore_localization.lift_expand_of {R : Type u_1} [monoid R] {S : submonoid R} [ore_localization.ore_set S] {C : Sort u_2} {P : R → ↥S → C} {hP : ∀ (r t : R) (s : ↥S) (ht : ↑s * t ∈ S), P r s = P (r * t) ⟨↑s * t, ht⟩} (r : R) (s : ↥S) :
ore_localization.lift_expand P hP (r /ₒ s) = P r s
source
def ore_localization.lift₂_expand {R : Type u_1} [monoid R] {S : submonoid R} [ore_localization.ore_set S] {C : Sort u_2} (P : R → ↥S → R → ↥S → C) (hP : ∀ (r₁ t₁ : R) (s₁ : ↥S) (ht₁ : ↑s₁ * t₁ ∈ S) (r₂ t₂ : R) (s₂ : ↥S) (ht₂ : ↑s₂ * t₂ ∈ S), P r₁ s₁ r₂ s₂ = P (r₁ * t₁) ⟨↑s₁ * t₁, ht₁⟩ (r₂ * t₂) ⟨↑s₂ * t₂, ht₂⟩) :
R[S⁻¹] → R[S⁻¹] → C

A version of lift_expand used to simultaneously lift functions with two arguments in ``R[S⁻¹]`.

Equations
source
@[simp]
theorem ore_localization.lift₂_expand_of {R : Type u_1} [monoid R] {S : submonoid R} [ore_localization.ore_set S] {C : Sort u_2} {P : R → ↥S → R → ↥S → C} {hP : ∀ (r₁ t₁ : R) (s₁ : ↥S) (ht₁ : ↑s₁ * t₁ ∈ S) (r₂ t₂ : R) (s₂ : ↥S) (ht₂ : ↑s₂ * t₂ ∈ S), P r₁ s₁ r₂ s₂ = P (r₁ * t₁) ⟨↑s₁ * t₁, ht₁⟩ (r₂ * t₂) ⟨↑s₂ * t₂, ht₂⟩} (r₁ : R) (s₁ : ↥S) (r₂ : R) (s₂ : ↥S) :
ore_localization.lift₂_expand P hP (r₁ /ₒ s₁) (r₂ /ₒ s₂) = P r₁ s₁ r₂ s₂
source
@[protected]
def ore_localization.mul {R : Type u_1} [monoid R] {S : submonoid R} [ore_localization.ore_set S] :
R[S⁻¹] → R[S⁻¹] → R[S⁻¹]

The multiplication on the Ore localization of monoids.

Equations
source
@[protected, instance]
def ore_localization.has_mul {R : Type u_1} [monoid R] {S : submonoid R} [ore_localization.ore_set S] :
has_mul R[S⁻¹]
Equations
source
theorem ore_localization.ore_div_mul_ore_div {R : Type u_1} [monoid R] {S : submonoid R} [ore_localization.ore_set S] {r₁ r₂ : R} {s₁ s₂ : ↥S} :
r₁ /ₒ s₁ * (r₂ /ₒ s₂) = r₁ * ore_localization.ore_num r₂ s₁ /ₒ (s₂ * ore_localization.ore_denom r₂ s₁)
source
theorem ore_localization.ore_div_mul_char {R : Type u_1} [monoid R] {S : submonoid R} [ore_localization.ore_set S] (r₁ r₂ : R) (s₁ s₂ : ↥S) (r' : R) (s' : ↥S) (huv : r₂ * ↑s' = ↑s₁ * r') :
r₁ /ₒ s₁ * (r₂ /ₒ s₂) = r₁ * r' /ₒ (s₂ * s')

A characterization lemma for the multiplication on the Ore localization, allowing for a choice of Ore numerator and Ore denominator.

source
def ore_localization.ore_div_mul_char' {R : Type u_1} [monoid R] {S : submonoid R} [ore_localization.ore_set S] (r₁ r₂ : R) (s₁ s₂ : ↥S) :
Σ' (r' : R) (s' : ↥S), r₂ * ↑s' = ↑s₁ * r' ∧ r₁ /ₒ s₁ * (r₂ /ₒ s₂) = r₁ * r' /ₒ (s₂ * s')

Another characterization lemma for the multiplication on the Ore localizaion delivering Ore witnesses and conditions bundled in a sigma type.

Equations
source
@[protected, instance]
def ore_localization.has_one {R : Type u_1} [monoid R] {S : submonoid R} [ore_localization.ore_set S] :
has_one R[S⁻¹]
Equations
source
@[protected]
theorem ore_localization.one_def {R : Type u_1} [monoid R] {S : submonoid R} [ore_localization.ore_set S] :
1 = 1 /ₒ 1
source
@[protected, instance]
def ore_localization.inhabited {R : Type u_1} [monoid R] {S : submonoid R} [ore_localization.ore_set S] :
inhabited R[S⁻¹]
Equations
source
@[protected, simp]
theorem ore_localization.div_eq_one' {R : Type u_1} [monoid R] {S : submonoid R} [ore_localization.ore_set S] {r : R} (hr : r ∈ S) :
r /ₒ ⟨r, hr⟩ = 1
source
@[protected, simp]
theorem ore_localization.div_eq_one {R : Type u_1} [monoid R] {S : submonoid R} [ore_localization.ore_set S] {s : ↥S} :
↑s /ₒ s = 1
source
@[protected]
theorem ore_localization.one_mul {R : Type u_1} [monoid R] {S : submonoid R} [ore_localization.ore_set S] (x : R[S⁻¹]) :
1 * x = x
source
@[protected]
theorem ore_localization.mul_one {R : Type u_1} [monoid R] {S : submonoid R} [ore_localization.ore_set S] (x : R[S⁻¹]) :
x * 1 = x
source
@[protected]
theorem ore_localization.mul_assoc {R : Type u_1} [monoid R] {S : submonoid R} [ore_localization.ore_set S] (x y z : R[S⁻¹]) :
x * y * z = x * (y * z)
source
@[protected, instance]
def ore_localization.monoid {R : Type u_1} [monoid R] {S : submonoid R} [ore_localization.ore_set S] :
monoid R[S⁻¹]
Equations
source
@[protected]
theorem ore_localization.mul_inv {R : Type u_1} [monoid R] {S : submonoid R} [ore_localization.ore_set S] (s s' : ↥S) :
↑s /ₒ s' * (↑s' /ₒ s) = 1
source
@[protected, simp]
theorem ore_localization.mul_one_div {R : Type u_1} [monoid R] {S : submonoid R} [ore_localization.ore_set S] {r : R} {s t : ↥S} :
r /ₒ s * (1 /ₒ t) = r /ₒ (t * s)
source
@[protected, simp]
theorem ore_localization.mul_cancel {R : Type u_1} [monoid R] {S : submonoid R} [ore_localization.ore_set S] {r : R} {s t : ↥S} :
r /ₒ s * (↑s /ₒ t) = r /ₒ t
source
@[protected, simp]
theorem ore_localization.mul_cancel' {R : Type u_1} [monoid R] {S : submonoid R} [ore_localization.ore_set S] {r₁ r₂ : R} {s t : ↥S} :
r₁ /ₒ s * (↑s * r₂ /ₒ t) = r₁ * r₂ /ₒ t
source
@[simp]
theorem ore_localization.div_one_mul {R : Type u_1} [monoid R] {S : submonoid R} [ore_localization.ore_set S] {p r : R} {s : ↥S} :
r /ₒ 1 * (p /ₒ s) = r * p /ₒ s
source
def ore_localization.numerator_unit {R : Type u_1} [monoid R] {S : submonoid R} [ore_localization.ore_set S] (s : ↥S) :
R[S⁻¹]ˣ

The fraction s /ₒ 1 as a unit in R[S⁻¹], where s : S.

Equations
source
def ore_localization.numerator_hom {R : Type u_1} [monoid R] {S : submonoid R} [ore_localization.ore_set S] :
R →* R[S⁻¹]

The multiplicative homomorphism from R to R[S⁻¹], mapping r : R to the fraction r /ₒ 1.

Equations
source
theorem ore_localization.numerator_hom_apply {R : Type u_1} [monoid R] {S : submonoid R} [ore_localization.ore_set S] {r : R} :
⇑ore_localization.numerator_hom r = r /ₒ 1
source
theorem ore_localization.numerator_is_unit {R : Type u_1} [monoid R] {S : submonoid R} [ore_localization.ore_set S] (s : ↥S) :
is_unit (⇑ore_localization.numerator_hom ↑s)
source
def ore_localization.universal_mul_hom {R : Type u_1} [monoid R] {S : submonoid R} [ore_localization.ore_set S] {T : Type u_2} [monoid T] (f : R →* T) (fS : ↥S →* Tˣ) (hf : ∀ (s : ↥S), ⇑f ↑s = ↑(⇑fS s)) :
R[S⁻¹] →* T

The universal lift from a morphism R →* T, which maps elements of S to units of T, to a morphism R[S⁻¹] →* T.

Equations
source
theorem ore_localization.universal_mul_hom_apply {R : Type u_1} [monoid R] {S : submonoid R} [ore_localization.ore_set S] {T : Type u_2} [monoid T] (f : R →* T) (fS : ↥S →* Tˣ) (hf : ∀ (s : ↥S), ⇑f ↑s = ↑(⇑fS s)) {r : R} {s : ↥S} :
⇑(ore_localization.universal_mul_hom f fS hf) (r /ₒ s) = ⇑f r * ↑(⇑fS s)⁻¹
source
theorem ore_localization.universal_mul_hom_commutes {R : Type u_1} [monoid R] {S : submonoid R} [ore_localization.ore_set S] {T : Type u_2} [monoid T] (f : R →* T) (fS : ↥S →* Tˣ) (hf : ∀ (s : ↥S), ⇑f ↑s = ↑(⇑fS s)) {r : R} :
⇑(ore_localization.universal_mul_hom f fS hf) (⇑ore_localization.numerator_hom r) = ⇑f r
source
theorem ore_localization.universal_mul_hom_unique {R : Type u_1} [monoid R] {S : submonoid R} [ore_localization.ore_set S] {T : Type u_2} [monoid T] (f : R →* T) (fS : ↥S →* Tˣ) (hf : ∀ (s : ↥S), ⇑f ↑s = ↑(⇑fS s)) (φ : R[S⁻¹] →* T) (huniv : ∀ (r : R), ⇑φ (⇑ore_localization.numerator_hom r) = ⇑f r) :
φ = ore_localization.universal_mul_hom f fS hf

The universal morphism universal_mul_hom is unique.

source
theorem ore_localization.ore_div_mul_ore_div_comm {R : Type u_1} [comm_monoid R] {S : submonoid R} [ore_localization.ore_set S] {r₁ r₂ : R} {s₁ s₂ : ↥S} :
r₁ /ₒ s₁ * (r₂ /ₒ s₂) = r₁ * r₂ /ₒ (s₁ * s₂)
source
@[protected, instance]
def ore_localization.comm_monoid {R : Type u_1} [comm_monoid R] {S : submonoid R} [ore_localization.ore_set S] :
comm_monoid R[S⁻¹]
Equations
source
@[protected]
def ore_localization.localization_map (R : Type u_1) [comm_monoid R] (S : submonoid R) [ore_localization.ore_set S] :
S.localization_map R[S⁻¹]

The morphism numerator_hom is a monoid localization map in the case of commutative R.

Equations
source
@[protected]
noncomputable def ore_localization.equiv_monoid_localization (R : Type u_1) [comm_monoid R] (S : submonoid R) [ore_localization.ore_set S] :
localization S ≃* R[S⁻¹]

If R is commutative, Ore localization and monoid localization are isomorphic.

Equations
source
@[protected, instance]
def ore_localization.has_add {R : Type u_1} [semiring R] {S : submonoid R} [ore_localization.ore_set S] :
has_add R[S⁻¹]
Equations
source
theorem ore_localization.ore_div_add_ore_div {R : Type u_1} [semiring R] {S : submonoid R} [ore_localization.ore_set S] {r r' : R} {s s' : ↥S} :
r /ₒ s + r' /ₒ s' = (r * ↑(ore_localization.ore_denom ↑s s') + r' * ore_localization.ore_num ↑s s') /ₒ (s * ore_localization.ore_denom ↑s s')
source
theorem ore_localization.ore_div_add_char {R : Type u_1} [semiring R] {S : submonoid R} [ore_localization.ore_set S] {r r' : R} (s s' : ↥S) (rb : R) (sb : ↥S) (h : ↑s * ↑sb = ↑s' * rb) :
r /ₒ s + r' /ₒ s' = (r * ↑sb + r' * rb) /ₒ (s * sb)

A characterization of the addition on the Ore localizaion, allowing for arbitrary Ore numerator and Ore denominator.

source
def ore_localization.ore_div_add_char' {R : Type u_1} [semiring R] {S : submonoid R} [ore_localization.ore_set S] (r r' : R) (s s' : ↥S) :
Σ' (r'' : R) (s'' : ↥S), ↑s * ↑s'' = ↑s' * r'' ∧ r /ₒ s + r' /ₒ s' = (r * ↑s'' + r' * r'') /ₒ (s * s'')

Another characterization of the addition on the Ore localization, bundling up all witnesses and conditions into a sigma type.

Equations
source
@[simp]
theorem ore_localization.add_ore_div {R : Type u_1} [semiring R] {S : submonoid R} [ore_localization.ore_set S] {r r' : R} {s : ↥S} :
r /ₒ s + r' /ₒ s = (r + r') /ₒ s
source
@[protected]
theorem ore_localization.add_assoc {R : Type u_1} [semiring R] {S : submonoid R} [ore_localization.ore_set S] (x y z : R[S⁻¹]) :
x + y + z = x + (y + z)
source
@[protected, instance]
def ore_localization.has_zero {R : Type u_1} [semiring R] {S : submonoid R} [ore_localization.ore_set S] :
has_zero R[S⁻¹]
Equations
source
@[protected]
theorem ore_localization.zero_def {R : Type u_1} [semiring R] {S : submonoid R} [ore_localization.ore_set S] :
0 = 0 /ₒ 1
source
@[simp]
theorem ore_localization.zero_div_eq_zero {R : Type u_1} [semiring R] {S : submonoid R} [ore_localization.ore_set S] (s : ↥S) :
0 /ₒ s = 0
source
@[protected]
theorem ore_localization.zero_add {R : Type u_1} [semiring R] {S : submonoid R} [ore_localization.ore_set S] (x : R[S⁻¹]) :
0 + x = x
source
@[protected]
theorem ore_localization.add_comm {R : Type u_1} [semiring R] {S : submonoid R} [ore_localization.ore_set S] (x y : R[S⁻¹]) :
x + y = y + x
source
@[protected, instance]
def ore_localization.add_comm_monoid {R : Type u_1} [semiring R] {S : submonoid R} [ore_localization.ore_set S] :
add_comm_monoid R[S⁻¹]
Equations
source
@[protected]
theorem ore_localization.zero_mul {R : Type u_1} [semiring R] {S : submonoid R} [ore_localization.ore_set S] (x : R[S⁻¹]) :
0 * x = 0
source
@[protected]
theorem ore_localization.mul_zero {R : Type u_1} [semiring R] {S : submonoid R} [ore_localization.ore_set S] (x : R[S⁻¹]) :
x * 0 = 0
source
@[protected]
theorem ore_localization.left_distrib {R : Type u_1} [semiring R] {S : submonoid R} [ore_localization.ore_set S] (x y z : R[S⁻¹]) :
x * (y + z) = x * y + x * z
source
theorem ore_localization.right_distrib {R : Type u_1} [semiring R] {S : submonoid R} [ore_localization.ore_set S] (x y z : R[S⁻¹]) :
(x + y) * z = x * z + y * z
source
@[protected, instance]
def ore_localization.semiring {R : Type u_1} [semiring R] {S : submonoid R} [ore_localization.ore_set S] :
semiring R[S⁻¹]
Equations
source
def ore_localization.universal_hom {R : Type u_1} [semiring R] {S : submonoid R} [ore_localization.ore_set S] {T : Type u_2} [semiring T] (f : R →+* T) (fS : ↥S →* Tˣ) (hf : ∀ (s : ↥S), ⇑f ↑s = ↑(⇑fS s)) :
R[S⁻¹] →+* T

The universal lift from a ring homomorphism f : R →+* T, which maps elements in S to units of T, to a ring homomorphism R[S⁻¹] →+* T. This extends the construction on monoids.

Equations
source
theorem ore_localization.universal_hom_apply {R : Type u_1} [semiring R] {S : submonoid R} [ore_localization.ore_set S] {T : Type u_2} [semiring T] (f : R →+* T) (fS : ↥S →* Tˣ) (hf : ∀ (s : ↥S), ⇑f ↑s = ↑(⇑fS s)) {r : R} {s : ↥S} :
⇑(ore_localization.universal_hom f fS hf) (r /ₒ s) = ⇑f r * ↑(⇑fS s)⁻¹
source
theorem ore_localization.universal_hom_commutes {R : Type u_1} [semiring R] {S : submonoid R} [ore_localization.ore_set S] {T : Type u_2} [semiring T] (f : R →+* T) (fS : ↥S →* Tˣ) (hf : ∀ (s : ↥S), ⇑f ↑s = ↑(⇑fS s)) {r : R} :
⇑(ore_localization.universal_hom f fS hf) (⇑ore_localization.numerator_hom r) = ⇑f r
source
theorem ore_localization.universal_hom_unique {R : Type u_1} [semiring R] {S : submonoid R} [ore_localization.ore_set S] {T : Type u_2} [semiring T] (f : R →+* T) (fS : ↥S →* Tˣ) (hf : ∀ (s : ↥S), ⇑f ↑s = ↑(⇑fS s)) (φ : R[S⁻¹] →+* T) (huniv : ∀ (r : R), ⇑φ (⇑ore_localization.numerator_hom r) = ⇑f r) :
φ = ore_localization.universal_hom f fS hf
source
@[protected]
def ore_localization.neg {R : Type u_1} [ring R] {S : submonoid R} [ore_localization.ore_set S] :
R[S⁻¹] → R[S⁻¹]

Negation on the Ore localization is defined via negation on the numerator.

Equations
source
@[protected, instance]
def ore_localization.has_neg {R : Type u_1} [ring R] {S : submonoid R} [ore_localization.ore_set S] :
has_neg R[S⁻¹]
Equations
source
@[protected, simp]
theorem ore_localization.neg_def {R : Type u_1} [ring R] {S : submonoid R} [ore_localization.ore_set S] (r : R) (s : ↥S) :
-(r /ₒ s) = -r /ₒ s
source
@[protected]
theorem ore_localization.add_left_neg {R : Type u_1} [ring R] {S : submonoid R} [ore_localization.ore_set S] (x : R[S⁻¹]) :
-x + x = 0
source
@[protected, instance]
def ore_localization.ring {R : Type u_1} [ring R] {S : submonoid R} [ore_localization.ore_set S] :
ring R[S⁻¹]
Equations
source
theorem ore_localization.numerator_hom_inj {R : Type u_1} [ring R] {S : submonoid R} [ore_localization.ore_set S] (hS : S ≤ non_zero_divisors R) :
function.injective ⇑ore_localization.numerator_hom
source
theorem ore_localization.nontrivial_of_non_zero_divisors {R : Type u_1} [ring R] {S : submonoid R} [ore_localization.ore_set S] [nontrivial R] (hS : S ≤ non_zero_divisors R) :
nontrivial R[S⁻¹]
source
@[protected, instance]
def ore_localization.nontrivial {R : Type u_1} [ring R] [nontrivial R] [ore_localization.ore_set (non_zero_divisors R)] :
nontrivial R[(non_zero_divisors R)⁻¹]
source
@[protected]
noncomputable def ore_localization.inv {R : Type u_1} [ring R] [nontrivial R] [ore_localization.ore_set (non_zero_divisors R)] [no_zero_divisors R] :
R[(non_zero_divisors R)⁻¹] → R[(non_zero_divisors R)⁻¹]

The inversion of Ore fractions for a ring without zero divisors, satisying 0⁻¹ = 0 and (r /ₒ r')⁻¹ = r' /ₒ r for r ≠ 0.

Equations
source
@[protected, instance]
noncomputable def ore_localization.has_inv {R : Type u_1} [ring R] [nontrivial R] [ore_localization.ore_set (non_zero_divisors R)] [no_zero_divisors R] :
has_inv R[(non_zero_divisors R)⁻¹]
Equations
source
@[protected]
theorem ore_localization.inv_def {R : Type u_1} [ring R] [nontrivial R] [ore_localization.ore_set (non_zero_divisors R)] [no_zero_divisors R] {r : R} {s : ↥(non_zero_divisors R)} :
(r /ₒ s)⁻¹ = dite (r = 0) (λ (hr : r = 0), 0) (λ (hr : ¬r = 0), ↑s /ₒ ⟨r, _⟩)
source
@[protected]
theorem ore_localization.mul_inv_cancel {R : Type u_1} [ring R] [nontrivial R] [ore_localization.ore_set (non_zero_divisors R)] [no_zero_divisors R] (x : R[(non_zero_divisors R)⁻¹]) (h : x ≠ 0) :
x * x⁻¹ = 1
source
@[protected]
theorem ore_localization.inv_zero {R : Type u_1} [ring R] [nontrivial R] [ore_localization.ore_set (non_zero_divisors R)] [no_zero_divisors R] :
0⁻¹ = 0
source
@[protected, instance]
noncomputable def ore_localization.division_ring {R : Type u_1} [ring R] [nontrivial R] [ore_localization.ore_set (non_zero_divisors R)] [no_zero_divisors R] :
division_ring R[(non_zero_divisors R)⁻¹]
Equations