Theorems · Theorem · commutative algebra

Algebra.TensorProduct.quotientTensorEquiv_apply_tmul

∀ {R : Type u_1} (S : Type u_2) (T : Type u_3) (A : Type u_4) [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : CommRing A] [inst_6 : Algebra R A]
  [inst_7 : Algebra S A] [inst_8 : IsScalarTower R S A] (I : Ideal A) (a : A) (t : T),
  (Algebra.TensorProduct.quotientTensorEquiv S T A I) ((Ideal.Quotient.mk I) a ⊗ₜ[R] t) =
    (Ideal.Quotient.mk (Ideal.map (algebraMap A (TensorProduct R A T)) I)) (a ⊗ₜ[R] t)

Defined in

Mathlib.RingTheory.TensorProduct.Quotient

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraCommRingAlgebraCommRingAlgebraAlgebraIsScalarTower