Theorems · Definition · linear algebra

Ideal.qoutMapEquivTensorQout

{R : Type u_1} →
  [inst : CommRing R] →
    (S : Type u_4) →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] → {I : Ideal R} → (S ⧸ Ideal.map (algebraMap R S) I) ≃ₗ[S] TensorProduct R S (R ⧸ I)

Let R be a commutative ring, S be an R-algebra, I is be ideal of R, then S ⧸ IS is isomorphic to S ⊗[R] (R ⧸ I) as S modules.

Defined in

Mathlib.LinearAlgebra.TensorProduct.Quotient

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebra