Theorem Algebra.TensorProduct.commRight_tmul

Modification history

2026-02-13 16:00
Mathlib/RingTheory/TensorProduct/Maps.lean
feat(RingTheory): `Algebra.FinitePresentation` descends along faithfully flat algebras (#35254) …
Added Algebra.TensorProduct.commRight_tmulView on Github →