# Commit 2021-06-25 10:35 1774cf95

View on Github →chore(data/complex/{module, is_R_or_C}, analysis/complex/basic): rationalize the structure provided for `conj`

and `of_real`

(#8014)
We have many bundled versions of the four operations associated with the complex-real interaction (real & imaginary parts, real-to-complex coercion `of_real`

, complex conjugation `conj`

).
This PR adjusts the versions provided, according to the following principles:

`conj`

is always an equivalence, there is never a need for the map version- Both
`of_real`

and`conj`

are`ℝ`

-algebra homomorphisms, and since this in typical applications requires no more imports than`ℝ`

-linear maps, they can entirely supersede the`ℝ`

-linear map versions. - Name according to the base map name together with an acronym for the bundled map type, for example
`conj_ae`

for`conj`

as an algebra-equivalence (this principle had been largely, but not entirely, followed previously). The following specific changes result: `quaternion.conj_alg_equiv`

renamed to`quaternion.conj_ae`

, likewise for`quaternion_algebra.conj_alg_equiv`

`complex.conj_li`

upgraded from a map to an equivalence`complex.conj_clm`

(continuous linear map) upgraded to`complex.conj_cle`

(continuous linear equivalence)`complex.conj_alg_equiv`

renamed to`complex.conj_ae`

`complex.conj_lm`

gone, use`complex.conj_ae`

instead`complex.of_real_lm`

(linear map) upgraded to`complex.of_real_am`

(algebra homomorphism)- all the same changes for
`is_R_or_C.*`

as for`complex.*`

Associated lemmas are also renamed.