mathlib3

1774cf95 - chore(data/complex/{module, is_R_or_C}, analysis/complex/basic): rationalize the structure provided for `conj` and `of_real` (#8014)

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.