Commit 2024-03-11 12:58 38c617fb

View on Github →

feat(LinearAlgebra/BilinearMap): restrict scalars (#6133) Generalizes the previous definition and moves it into LinearAlgebra/BilinearMap.

Estimated changes

Modified Mathlib/Algebra/Algebra/Bilinear.lean

deleted def LinearMap.restrictScalars₁₂

Modified Mathlib/LinearAlgebra/BilinearMap.lean

added def LinearMap.restrictScalars₁₂

added theorem LinearMap.restrictScalars₁₂_inj

added theorem LinearMap.restrictScalars₁₂_injective

Modified Mathlib/LinearAlgebra/QuadraticForm/Basic.lean