Commit 2023-01-24 03:14 468b141b

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).