Documentation

Mathlib.RingTheory.TensorProduct.Quotient

Interaction between quotients and tensor products for algebras #

This files proves algebra analogs of the isomorphisms in Mathlib.LinearAlgebra.TensorProduct.Quotient.

Main results #

B ⊗[A] (A ⧸ I) is isomorphic as an A-algebra to B ⧸ I B.

Equations
Instances For