Theorems · Theorem · commutative algebra

Ideal.pi_mkQ_rTensor

∀ {R : Type u_1} [inst : CommRing R] {ι : Type u_2} (M : Type u_3) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (I : ι → Ideal R) [inst_3 : Fintype ι] [inst_4 : DecidableEq ι],
  LinearMap.rTensor M (LinearMap.pi fun i => Submodule.mkQ (I i)) =
    ↑(TensorProduct.piLeft R M fun i => R ⧸ I i).symm ∘ₗ
      (LinearMap.pi fun i => (TensorProduct.mk R (R ⧸ I i) M) 1) ∘ₗ ↑(TensorProduct.lid R M)

Defined in

Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModuleFintypeDecidableEq