Theorems · Theorem · commutative algebra

LocalizedModule.mk_eq

∀ {R : Type u} [inst : CommSemiring R] {S : Submonoid R} {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {m m' : M} {s s' : ↥S}, LocalizedModule.mk m s = LocalizedModule.mk m' s' ↔ ∃ u, u • s' • m = u • s • m'

Defined in

Mathlib.Algebra.Module.LocalizedModule.Basic

Cited by

15 results in Mathlib

Foundations

Depth 24 from the axioms · uses propext, Quot.sound

Assumes

CommSemiringAddCommMonoidModule