Theorems · Theorem · commutative algebra

LocalizedModule.equivTensorProduct_symm_apply_tmul

∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (x : M) (r : R) (s : ↥S),
  (LocalizedModule.equivTensorProduct S M).symm (Localization.mk r s ⊗ₜ[R] x) = r • LocalizedModule.mk x s

Defined in

Mathlib.RingTheory.Localization.BaseChange

Cited by

2 results in Mathlib

Foundations

Depth 75 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringAddCommMonoidModule