Theorems · Definition · commutative algebra

QuotSMulTop.algebraMapTensorEquivTensorQuotSMulTop

{R : Type u_3} →
  [inst : CommRing R] →
    (r : R) →
      (M : Type u_1) →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            (S : Type u_2) →
              [inst_3 : CommRing S] →
                [inst_4 : Algebra R S] →
                  QuotSMulTop ((algebraMap R S) r) (TensorProduct R S M) ≃ₗ[S] TensorProduct R S (QuotSMulTop r M)

Let R be a commutative ring, M be an R-module, S be an R-algebra, then S ⊗[R] (M/rM) is isomorphic to (S ⊗[R] M)⧸r(S ⊗[R] M) as S-modules.

Defined in

Mathlib.RingTheory.QuotSMulTop

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModuleCommRingAlgebra