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

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

`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

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

Equations

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

Instances For