Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-09 06:06 ca5e55cc

View on Github →

feat(linear_algebra/basis): basis.ext, basis.ext' for semilinear maps (#11317) Extend basis.ext and basis.ext' to apply to the general (semilinear) case of linear_map and linear_equiv.

Estimated changes