mathlib

16a9031a - refactor(data/complex/*): replace `complex.conj` and `is_R_or_C.conj` with star (#9640)

refactor(data/complex/*): replace `complex.conj` and `is_R_or_C.conj` with star (#9640) This PR replaces `complex.conj` and `is_R_or_C.conj` by the star operation defined in `algebra/star`. Both of these are replaced with `star_ring_aut`, which is also made available under the notation `conj` defined in the locale `complex_conjugate`. This effectively also upgrades conj from a `ring_hom` to a `ring_aut`. Fixes #9421