Documentation

Mathlib.RingTheory.OreLocalization.OreSet

(Left) Ore sets and rings #

This file contains results on left Ore sets for rings and monoids with zero.

References #

source
🔸 coverage
@[implicit_reducible]
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.

Instances For
    source
    🔸 coverage
    @[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
      source
      🔸 coverage
      @[implicit_reducible]
      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.

      Instances For
        source
        📐 coverage
        theorem OreLocalization.nonempty_oreSet_iff {R : Type u_1} [Monoid R] {S : Submonoid R} :
        Nonempty (OreSet S) ↔ (∀ (r₁ r₂ : R) (s : ↥S), r₁ * ↑s = r₂ * ↑s → ∃ (s' : ↥S), ↑s' * r₁ = ↑s' * r₂) ∧ ∀ (r : R) (s : ↥S), ∃ (r' : R) (s' : ↥S), ↑s' * r = r' * ↑s
        source
        📐 coverage
        theorem OreLocalization.nonempty_oreSet_iff_of_noZeroDivisors {R : Type u_1} [Ring R] [NoZeroDivisors R] {S : Submonoid R} :
        Nonempty (OreSet S) ↔ ∀ (r : R) (s : ↥S), ∃ (r' : R) (s' : ↥S), ↑s' * r = r' * ↑s