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.

Equations
    Instances For
      source
      noncomputable instance OreLocalization.inv' {R : Type u_1} [MonoidWithZero R] [Nontrivial R] [OreSet (nonZeroDivisors R)] [NoZeroDivisors R] :
      Inv (OreLocalization (nonZeroDivisors R) R)
      Equations
        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
        noncomputable instance OreLocalization.instGroupWithZeroNonZeroDivisors {R : Type u_1} [MonoidWithZero R] [Nontrivial R] [OreSet (nonZeroDivisors R)] [NoZeroDivisors R] :
        GroupWithZero (OreLocalization (nonZeroDivisors R) R)
        Equations
          source
          noncomputable instance OreLocalization.instCommGroupWithZeroNonZeroDivisors {R : Type u_1} [CommMonoidWithZero R] [Nontrivial R] [OreSet (nonZeroDivisors R)] [NoZeroDivisors R] :
          CommGroupWithZero (OreLocalization (nonZeroDivisors R) R)
          Equations