Commit 2021-06-25 10:35 1774cf95

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.