OreLocalization — Mathlib

English

The relation oreEqv is an equivalence relation on X × S, i.e. it is reflexive, symmetric, and transitive.

Русский

Отношение oreEqv образует эквивалентность на X × S: оно рефлексивно, симметрично и транзитивно.

LaTeX

$$\text{oreEqv is an equivalence relation on } X \times S$$

Lean4

/-- The Ore localization of a monoid and a submonoid fulfilling the Ore condition. -/
@[to_additive AddOreLocalization /-- The Ore localization of an additive monoid and a submonoid
    fulfilling the Ore condition. -/
    ]
def OreLocalization {R : Type*} [Monoid R] (S : Submonoid R) [OreSet S] (X : Type*) [MulAction R X] :=
  Quotient (OreLocalization.oreEqv S X)

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