Theorems · Definition · ring theory

OreLocalization

{R : Type u_1} →
  [inst : Monoid R] →
    (S : Submonoid R) → [OreLocalization.OreSet S] → (X : Type u_2) → [MulAction R X] → Type (max u_1 u_2)

The Ore localization of a monoid and a submonoid fulfilling the Ore condition.

Defined in

Mathlib.GroupTheory.OreLocalization.Basic

Cited by

90 results in Mathlib

Foundations

Depth 20 from the axioms · uses propext

Assumes

MonoidOreLocalization.OreSetMulAction