mathlib3

3fb5b82e - feat(algebra/star/basic): change `star_ring_aut` (notably, complex conjugation) from `ring_equiv` to `ring_hom` and make type argument explicit (#11418)

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 ```lean def star_ring_aut [comm_semiring R] [star_ring R] : ring_aut R := ``` to ```lean 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`.