Theorems · Definition · linear algebra

TensorProduct.quotTensorEquivQuotSMul

{R : Type u_1} →
  (M : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (I : Ideal R) → TensorProduct R (R ⧸ I) M ≃ₗ[R] M ⧸ I • ⊤

Left tensoring a module with a quotient of the ring is the same as quotienting that module by the corresponding submodule.

Defined in

Mathlib.LinearAlgebra.TensorProduct.Quotient

Cited by

13 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModule