Commit 2023-07-28 13:43 6cb636b7
View on Github →chore(RingTheory/TensorProduct): golf a proof (#6211)
This follows the approach taken in Algebra/DirectSum/Ring, which allows avoiding tedious induction by instead conjuring a weird equality of morphisms and using ext.