Theorems · Definition · ring theory

OreLocalization.hsmul

{R : Type u_1} →
  {M : Type u_3} →
    {X : Type u_4} →
      [inst : Monoid M] →
        {S : Submonoid M} →
          [inst_1 : OreLocalization.OreSet S] →
            [inst_2 : MulAction M X] → [SMul R M] → R → OreLocalization S X → OreLocalization S X

Scalar multiplication in a monoid localization.

Defined in: Mathlib.GroupTheory.OreLocalization.Basic
Cited by: 0 results in Mathlib
Foundations: Depth 31 from the axioms · uses propext, Quot.sound
Assumes: Monoid OreLocalization.OreSet MulAction SMul

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites9

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

Monoidstatement and proof · cited by 3,887
Submonoidstatement and proof · cited by 3,086
MulActionstatement and proof · cited by 1,294
OreLocalization.OreSetstatement and proof · cited by 92
OreLocalizationstatement · cited by 90
OreLocalization.oreDivproof · cited by 72
OreLocalization.oreNumproof · cited by 11
OreLocalization.oreDenomproof · cited by 11
OreLocalization.liftExpandproof · cited by 1

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.