Def LinearMap.linMulLin

Modification history

2024-02-08 05:11
Mathlib/LinearAlgebra/BilinearMap.lean
chore(LinearAlgebra/QuadraticForm): fixups to #10097 (#10167) …
Deleted LinearMap.linMulLinView on Github →
2024-02-01 12:43
Mathlib/LinearAlgebra/BilinearMap.lean
refactor(LinearAlgebra/QuadraticForm/Basic): Use bilinear maps for the companion (#10097) …
Added LinearMap.linMulLinView on Github →