Def LinearMap.mul'

Modification history

2025-07-03 01:14
Mathlib/Algebra/Algebra/Bilinear.lean
refactor: remove `suppress_compilation` from TensorProduct (#26642) …
Added LinearMap.mul'View on Github →
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 →