Commit 2022-01-16 09:33 3fb5b82e
View on Github →feat(algebra/star/basic): change star_ring_aut (notably, complex conjugation) from ring_equiv to ring_hom and make type argument explicit (#11418)
Change the underlying object notated by conj from
def star_ring_aut [comm_semiring R] [star_ring R] : ring_aut R :=
to
def star_ring_end [comm_semiring R] [star_ring R] : R →+* R :=
and also make the R argument explicit. These two changes allow the notation for conjugate-linear maps, E →ₗ⋆[R] F and variants, to pretty-print, see
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Pretty.20printer.20omits.20notation
This is a partial reversion of #9640, in which complex conjugation was upgraded from ring_hom to ring_equiv.