Notation for star-linear maps

This is in a separate file as it is not needed until much later, and avoids importing the theory of star operations unnecessarily early.

def «term_→ₗ⋆[_]_» : Lean.TrailingParserDescr

M →ₗ⋆[R] N is the type of R-conjugate-linear maps from M to N.

def «term_≃ₗ⋆[_]_» : Lean.TrailingParserDescr

The notation M ≃ₗ⋆[R] M₂ denotes the type of star-linear equivalences between M and M₂ over the ⋆ endomorphism of the underlying starred ring R.