Def LinearMap.mul'

Modification history

2023-10-11 09:58
Mathlib/Algebra/Algebra/Bilinear.lean
feat: use suppress_compilation in tensor products (#7504) …
Deleted LinearMap.mul'View on Github →
2023-03-01 18:09
Mathlib/Algebra/Algebra/Bilinear.lean
feat: port Algebra.Algebra.Bilinear (#2552)
Added LinearMap.mul'View on Github →