Commit 2021-10-21 23:04 16a9031a
View on Github →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