(Left) Ore sets and rings #
This file contains results on left Ore sets for rings and monoids with zero.
References #
- https://ncatlab.org/nlab/show/Ore+set
def
OreLocalization.oreSetOfIsCancelMulZero
{R : Type u_1}
[MonoidWithZero R]
[IsCancelMulZero R]
{S : Submonoid R}
(oreNum : R → ↥S → R)
(oreDenom : R → ↥S → ↥S)
(ore_eq : ∀ (r : R) (s : ↥S), ↑(oreDenom r s) * r = oreNum r s * ↑s)
:
OreSet S
Cancellability in monoids with zeros can act as a replacement for the ore_right_cancel
condition of an ore set.
Equations
- OreLocalization.oreSetOfIsCancelMulZero oreNum oreDenom ore_eq = { ore_right_cancel := ⋯, oreNum := oreNum, oreDenom := oreDenom, ore_eq := ore_eq }
Instances For
@[deprecated OreLocalization.oreSetOfIsCancelMulZero (since := "2026-01-12")]
def
OreLocalization.oreSetOfCancelMonoidWithZero
{R : Type u_1}
[MonoidWithZero R]
[IsCancelMulZero R]
{S : Submonoid R}
(oreNum : R → ↥S → R)
(oreDenom : R → ↥S → ↥S)
(ore_eq : ∀ (r : R) (s : ↥S), ↑(oreDenom r s) * r = oreNum r s * ↑s)
:
OreSet S
Alias of OreLocalization.oreSetOfIsCancelMulZero.
Cancellability in monoids with zeros can act as a replacement for the ore_right_cancel
condition of an ore set.
Instances For
def
OreLocalization.oreSetOfNoZeroDivisors
{R : Type u_1}
[Ring R]
[NoZeroDivisors R]
{S : Submonoid R}
(oreNum : R → ↥S → R)
(oreDenom : R → ↥S → ↥S)
(ore_eq : ∀ (r : R) (s : ↥S), ↑(oreDenom r s) * r = oreNum r s * ↑s)
:
OreSet S
In rings without zero divisors, the first (cancellability) condition is always fulfilled, it suffices to give a proof for the Ore condition itself.
Equations
- OreLocalization.oreSetOfNoZeroDivisors oreNum oreDenom ore_eq = OreLocalization.oreSetOfIsCancelMulZero oreNum oreDenom ore_eq