Theorem Equiv.tensorProductComm_def

Modification history

2026-02-12 09:07
Mathlib/LinearAlgebra/TensorProduct/Basic.lean
refactor(LinearAlgebra/TensorProduct): split large file (#34798) …
Modified Equiv.tensorProductComm_defView on Github →
2025-12-31 12:47
Mathlib/LinearAlgebra/TensorProduct/Basic.lean
feat: transfer `Coalgebra.IsCocomm` across an `Equiv` (#33139) …
Added Equiv.tensorProductComm_defView on Github →