Theorem TensorProduct.Algebra.mul'_comp_tensorTensorTensorComm

Modification history

2025-08-31 17:16
Mathlib/RingTheory/TensorProduct/Basic.lean
chore(RingTheory/TensorProduct/Basic): generalize result (#29158) …
Modified TensorProduct.Algebra.mul'_comp_tensorTensorTensorCommView on Github →
2025-02-12 21:23
Mathlib/RingTheory/TensorProduct/Basic.lean
feat: tensor products of Hopf algebras (#12009) …
Added TensorProduct.Algebra.mul'_comp_tensorTensorTensorCommView on Github →