Theorem Equiv.tensorProductAssoc_def

Modification history

2026-08-10 23:43
Mathlib/LinearAlgebra/TensorProduct/Associator.lean
feat: generalize transfer instance type class assumptions (#42291) …
Deleted Equiv.tensorProductAssoc_defView on Github →
2025-12-31 12:47
Mathlib/LinearAlgebra/TensorProduct/Associator.lean
feat: transfer `Coalgebra.IsCocomm` across an `Equiv` (#33139) …
Modified Equiv.tensorProductAssoc_defView on Github →
2025-12-19 16:47
Mathlib/LinearAlgebra/TensorProduct/Associator.lean
feat(RingTheory): transfer `Coalgebra` across an `Equiv` (#32965)
Added Equiv.tensorProductAssoc_defView on Github →