mathlib3

ca5e55cc - feat(linear_algebra/basis): `basis.ext`, `basis.ext'` for semilinear maps (#11317)

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`.