Theorem LinearEquiv.tensorProductComm_def

Modification history

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