mathlib3

55a11604 - feat(linear_algebra): add notation for star-linear maps (#9875)

feat(linear_algebra): add notation for star-linear maps (#9875) This PR adds the notation `M →ₗ⋆[R] N`, `M ≃ₗ⋆[R] N`, etc, to denote star-linear maps/equivalences, i.e. semilinear maps where the ring hom is `star`. A special case of this are conjugate-linear maps when `R = ℂ`. Co-authored-by: Heather Macbeth <hmacbeth1@fordham.edu> Co-authored-by: Frédéric Dupuis <dupuisf@iro.umontreal.ca>