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.

Estimated changes

added def complex.conj_cle
added theorem complex.conj_cle_apply
added theorem complex.conj_cle_coe
added theorem complex.conj_cle_norm
deleted def complex.conj_clm
deleted theorem complex.conj_clm_apply
deleted theorem complex.conj_clm_coe
deleted theorem complex.conj_clm_norm
deleted def complex.conj_li
deleted theorem complex.conj_li_apply
added def complex.conj_lie
added theorem complex.conj_lie_apply
modified theorem complex.continuous_conj
modified theorem complex.continuous_of_real
modified theorem complex.isometry_conj
modified theorem complex.of_real_clm_apply
modified theorem complex.of_real_clm_coe
modified def complex.of_real_li