Interaction between quotients and tensor products for algebras #
This files proves algebra analogs of the isomorphisms in
Mathlib.LinearAlgebra.TensorProduct.Quotient
.
Main results #
Algebra.TensorProduct.quotIdealMapEquivTensorQuot
:B ⧸ (I.map <| algebraMap A B) ≃ₐ[B] B ⊗[A] (A ⧸ I)