English
Star acts as a ring endomorphism for commutative R.
Русский
Звезда действует как окончательное отображение колца для коммутативного R.
LaTeX
$$$$ \text{starRingEnd} : R \to^+_R R \text{ is a ring endomorphism}. $$$$
Lean4
/-- `star` as a ring endomorphism, for commutative `R`. This is used to denote complex
conjugation, and is available under the notation `conj` in the scope `ComplexConjugate`.
Note that this is the preferred form (over `starRingAut`, available under the same hypotheses)
because the notation `E →ₗ⋆[R] F` for an `R`-conjugate-linear map (short for
`E →ₛₗ[starRingEnd R] F`) does not pretty-print if there is a coercion involved, as would be the
case for `(↑starRingAut : R →* R)`. -/
def starRingEnd : R →+* R :=
@starRingAut R _ _
