Commit 2025-04-24 23:11 0d05f2a9

View on Github →

feat (LinearAlgebra/BilinearMap): restrict scalars and range of a linear map (#24345) This PR introduces restrictScalarsRange, which is a linear map that restricts the scalars and range of a linear map. The function previously named restrictScalarsRange is about bilinear maps, and is renamed restrictScalarsRange₂.

Estimated changes

Modified Mathlib/LinearAlgebra/BilinearMap.lean

modified theorem LinearMap.eq_restrictScalarsRange_iff

added theorem LinearMap.eq_restrictScalarsRange₂_iff

modified theorem LinearMap.restrictScalarsRange_apply

modified theorem LinearMap.restrictScalarsRange_apply_eq_zero_iff

added theorem LinearMap.restrictScalarsRange₂_apply

added theorem LinearMap.restrictScalarsRange₂_apply_eq_zero_iff

Modified Mathlib/LinearAlgebra/PerfectPairing/Restrict.lean

Modified Mathlib/LinearAlgebra/RootSystem/RootPositive.lean