Theorem Algebra.TensorProduct.Algebra.TensorProduct.commRight_symm_tmul

Modification history

2026-05-25 15:44
Mathlib/RingTheory/TensorProduct/Maps.lean
fix: decls with a non-consecutive duplicate namespace (#39794) …
Deleted Algebra.TensorProduct.Algebra.TensorProduct.commRight_symm_tmulView on Github →
2026-02-13 16:00
Mathlib/RingTheory/TensorProduct/Maps.lean
feat(RingTheory): `Algebra.FinitePresentation` descends along faithfully flat algebras (#35254) …
Added Algebra.TensorProduct.Algebra.TensorProduct.commRight_symm_tmulView on Github →