# Notation for star-linear maps #

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

`M →ₗ⋆[R] N`

is the type of `R`

-conjugate-linear maps from `M`

to `N`

.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

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`

.

## Equations

- One or more equations did not get rendered due to their size.