mathlib

468b141b - refactor(analysis/complex/basic, data/complex/is_R_or_C): downgrade imports (#18217)

refactor(analysis/complex/basic, data/complex/is_R_or_C): downgrade imports (#18217) The files `data/complex/is_R_or_C` and `analysis/complex/basic` are imported widely across the analysis library: for example - `data/complex/is_R_or_C` into inner product spaces - `analysis/complex/basic` into the construction of `rpow` and thence into Lp spaces and the Bochner integral So it is useful (for the port and for compilation time) to make them as elementary as possible. Currently they both import `analysis/normed_space/operator_norm` and `analysis/normed_space/finite_dimension`, rather heavy imports, but use quite little from these files: they provide lemmas about the operator norms of `re`/`im`/`conj`/`of_real`, and get cheaply some facts about the topology of `ℂ`/`is_R_or_C` via real-finite-dimensionality. This PR splits both files. - `analysis/complex/basic` is split in place, with substantially downgraded imports, and with a few heavier lemmas moved to `analysis/complex/operator_norm`. (And a few lemmas moved earlier to `data/complex/module`.). I wrote direct proofs for the completeness and properness of `ℂ` so that these facts can remain available by importing this file, even though with heavier imports these facts can be deduced from the real-finite-dimensionality of `ℂ`. - `data/complex/is_R_or_C` is split into `data/is_R_or_C/basic` (lightweight file containing most of the former file) and `data/is_R_or_C/lemmas` (a few heavier lemmas). Also rename `equiv_real_prod_add_hom_lm` to `equiv_real_prod_lm` (an apparent typo), and `equiv_real_prodₗ` to `equiv_real_prod_clm` (also an apparent error since in our naming convention `ₗ` usually refers to linearity, not continuous-linearity).