Ore Localization over nonZeroDivisors in monoids with zeros.

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)

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)

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)

instance OreLocalization.nontrivial {R : Type u_1} [MonoidWithZero R] [Nontrivial R] [OreSet (nonZeroDivisors R)] : Nontrivial (OreLocalization (nonZeroDivisors R) R)

@[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

• OreLocalization.inv = OreLocalization.liftExpand (fun (r : R) (s : ↥(nonZeroDivisors R)) => if hr : r = 0 then 0 else ↑s /ₒ ⟨r, ⋯⟩) ⋯

@[instance_reducible]

noncomputable instance OreLocalization.inv' {R : Type u_1} [MonoidWithZero R] [Nontrivial R] [OreSet (nonZeroDivisors R)] [NoZeroDivisors R] : Inv (OreLocalization (nonZeroDivisors R) R)

Equations

• OreLocalization.inv' = { inv := OreLocalization.inv }

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, ⋯⟩

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

theorem OreLocalization.inv_zero {R : Type u_1} [MonoidWithZero R] [Nontrivial R] [OreSet (nonZeroDivisors R)] [NoZeroDivisors R] : 0⁻¹ = 0

@[instance_reducible]

noncomputable instance OreLocalization.instGroupWithZeroNonZeroDivisors {R : Type u_1} [MonoidWithZero R] [Nontrivial R] [OreSet (nonZeroDivisors R)] [NoZeroDivisors R] : GroupWithZero (OreLocalization (nonZeroDivisors R) R)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance OreLocalization.instCommGroupWithZeroNonZeroDivisors {R : Type u_1} [CommMonoidWithZero R] [Nontrivial R] [OreSet (nonZeroDivisors R)] [NoZeroDivisors R] : CommGroupWithZero (OreLocalization (nonZeroDivisors R) R)

Equations

• One or more equations did not get rendered due to their size.