https://leanprover-community.github.io/theories/linear_algebra.html doesn't mention semilinear maps.
https://leanprover-community.github.io/theories/linear_algebra.html doesn't mention semilinear maps.