Mathlib Map

Theorems · Definition · ring theory

OreLocalization.oreDiv

{R : Type u_1} →
  [inst : Monoid R] →
    {S : Submonoid R} →
      [inst_1 : OreLocalization.OreSet S] → {X : Type u_2} → [inst_2 : MulAction R X] → X → ↥S → OreLocalization S X

The division in the Ore localization X[S⁻¹], as a fraction of an element of X and S.

Defined in
Mathlib.GroupTheory.OreLocalization.Basic
Cited by
72 results in Mathlib
Foundations
Depth 21 from the axioms · uses propext
Assumes
MonoidOreLocalization.OreSetMulAction
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Localization.mk · cited by 110Localization.mkLocalizedModule.mk · cited by 73LocalizedModule.mkOreLocalization.ind · cited by 18OreLocalization.indLocalizedModule.mk_eq · cited by 15LocalizedModule.mk_eqLocalizedModule.smul'_mk · cited by 13LocalizedModule.smul'_mkOreLocalization.one_def · cited by 10OreLocalization.one_defOreLocalization.oreDiv_eq_iff · cited by 9OreLocalization.oreDiv_eq…OreLocalization.zero_oreDiv · cited by 8OreLocalization.zero_oreD…OreLocalization.numeratorHom · cited by 8OreLocalization.numerator…OreLocalization.oreDiv_mul_char · cited by 8OreLocalization.oreDiv_mu…OreLocalization.oreDiv_smul_char · cited by 8OreLocalization.oreDiv_sm…OreLocalization.zero_def · cited by 6OreLocalization.zero_defLocalizedModule.mk_add_mk · cited by 5LocalizedModule.mk_add_mkLocalization.smul_mk · cited by 4Localization.smul_mkOreLocalization.add_oreDiv · cited by 4OreLocalization.add_oreDivMonoid · cited by 3887MonoidSubmonoid · cited by 3086SubmonoidMulAction · cited by 1294MulActionOreLocalization.OreSet · cited by 92OreLocalization.OreSetOreLocalization · cited by 90OreLocalizationOreLocalization.oreDivCITED BYCITES

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by84

Results whose statement or proof uses this declaration.