Documentation

Mathlib.RingTheory.OreLocalization.NonZeroDivisors

Ore Localization over nonZeroDivisors in monoids with zeros. #

source
theorem OreLocalization.nontrivial_of_nonZeroDivisorsLeft {R : Type u_1} [MonoidWithZero R] {S : Submonoid R} [OreSet S] [Nontrivial R] (hS : S ≤ nonZeroDivisorsLeft R) :
Nontrivial (OreLocalization S R)
source
theorem OreLocalization.nontrivial_of_nonZeroDivisorsRight {R : Type u_1} [MonoidWithZero R] {S : Submonoid R} [OreSet S] [Nontrivial R] (hS : S ≤ nonZeroDivisorsRight R) :
Nontrivial (OreLocalization S R)
source
theorem OreLocalization.nontrivial_of_nonZeroDivisors {R : Type u_1} [MonoidWithZero R] {S : Submonoid R} [OreSet S] [Nontrivial R] (hS : S ≤ nonZeroDivisors R) :
Nontrivial (OreLocalization S R)
source
instance OreLocalization.nontrivial {R : Type u_1} [MonoidWithZero R] [Nontrivial R] [OreSet (nonZeroDivisors R)] :
Nontrivial (OreLocalization (nonZeroDivisors R) R)
source
@[irreducible]
noncomputable def OreLocalization.inv {R : Type u_1} [MonoidWithZero R] [Nontrivial R] [OreSet (nonZeroDivisors R)] [NoZeroDivisors R] :
OreLocalization (nonZeroDivisors R) R → OreLocalization (nonZeroDivisors R) R

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

Instances For
    source
    @[instance_reducible]
    noncomputable instance OreLocalization.inv' {R : Type u_1} [MonoidWithZero R] [Nontrivial R] [OreSet (nonZeroDivisors R)] [NoZeroDivisors R] :
    Inv (OreLocalization (nonZeroDivisors R) R)
    source
    theorem OreLocalization.inv_def {R : Type u_1} [MonoidWithZero R] [Nontrivial R] [OreSet (nonZeroDivisors R)] [NoZeroDivisors R] {r : R} {s : ↥(nonZeroDivisors R)} :
    (r /ₒ s)⁻¹ = if hr : r = 0 then 0 else ↑s /ₒ ⟨r, ⋯⟩
    source
    theorem OreLocalization.mul_inv_cancel {R : Type u_1} [MonoidWithZero R] [Nontrivial R] [OreSet (nonZeroDivisors R)] [NoZeroDivisors R] (x : OreLocalization (nonZeroDivisors R) R) (h : x ≠ 0) :
    x * x⁻¹ = 1
    source
    theorem OreLocalization.inv_zero {R : Type u_1} [MonoidWithZero R] [Nontrivial R] [OreSet (nonZeroDivisors R)] [NoZeroDivisors R] :
    0⁻¹ = 0
    source
    @[instance_reducible]
    noncomputable instance OreLocalization.instGroupWithZeroNonZeroDivisors {R : Type u_1} [MonoidWithZero R] [Nontrivial R] [OreSet (nonZeroDivisors R)] [NoZeroDivisors R] :
    GroupWithZero (OreLocalization (nonZeroDivisors R) R)
    source
    @[instance_reducible]
    noncomputable instance OreLocalization.instCommGroupWithZeroNonZeroDivisors {R : Type u_1} [CommMonoidWithZero R] [Nontrivial R] [OreSet (nonZeroDivisors R)] [NoZeroDivisors R] :
    CommGroupWithZero (OreLocalization (nonZeroDivisors R) R)