Theorem LinearEquiv.tensorProductAssoc_def

Modification history

2026-08-10 23:43
Mathlib/LinearAlgebra/TensorProduct/Associator.lean
feat: generalize transfer instance type class assumptions (#42291) …
Added LinearEquiv.tensorProductAssoc_defView on Github →