Def LinearMap.restrictScalars₁₂

Modification history

2024-03-11 12:58
Mathlib/Algebra/Algebra/Bilinear.lean
feat(LinearAlgebra/BilinearMap): restrict scalars (#6133) …
Modified LinearMap.restrictScalars₁₂View on Github →
2024-02-08 05:11
Mathlib/Algebra/Algebra/Bilinear.lean
chore(LinearAlgebra/QuadraticForm): fixups to #10097 (#10167) …
Added LinearMap.restrictScalars₁₂View on Github →