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







leanprover-community/mathlib,leanprover-community/mathlib