Theorems · Definition · commutative algebra

LocalizedModule.mk

{R : Type u} →
  [inst : CommSemiring R] →
    {S : Submonoid R} → {M : Type v} → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → M → ↥S → LocalizedModule S M

The canonical map sending (m, s) ↦ m/s

Defined in

Mathlib.Algebra.Module.LocalizedModule.Basic

Cited by

73 results in Mathlib

Foundations

Depth 22 from the axioms · uses propext

Assumes

CommSemiringAddCommMonoidModule