Def LinearMap.dualProd

Modification history

2024-02-26 00:38

Mathlib/LinearAlgebra/QuadraticForm/Dual.lean

refactor(LinearAlgebra/QuadraticForm): Replace `BilinForm` with a scalar valued bi `LinearMap` (#10238) …

Modified LinearMap.dualProd View on Github →

2024-02-01 12:43

Mathlib/LinearAlgebra/QuadraticForm/Dual.lean

refactor(LinearAlgebra/QuadraticForm/Basic): Use bilinear maps for the companion (#10097) …

Added LinearMap.dualProd View on Github →