oreSetOfNoZeroDivisors — Mathlib

English

In a NoZeroDivisors ring, oreSetOfNoZeroDivisors produces an OreSet S from compatible Ore data.

Русский

В кольце без нулевых делителей, oreSetOfNoZeroDivisors порождает OreSet S из совместимых данных Ore.

LaTeX

$$oreSetOfNoZeroDivisors(R, S, oreNum, oreDenom, ore_eq) : OreSet S$$

Lean4

/-- In rings without zero divisors, the first (cancellability) condition is always fulfilled,
it suffices to give a proof for the Ore condition itself. -/
def oreSetOfNoZeroDivisors {R : Type*} [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 :=
  letI : CancelMonoidWithZero R := NoZeroDivisors.toCancelMonoidWithZero
  oreSetOfCancelMonoidWithZero oreNum oreDenom ore_eq

Похожие утверждения