Commit 2025-02-28 20:41 f4011100

chore(NumberField/CanonicalEmbedding): Fix naming (#21629) When dealing with the mixed space, a lot of results depend on whether the infinite place considered is real or is complex and thus are duplicated using the ending apply_of_isReal or apply_of_isComplex in their names. However, the spelling apply_ofIsReal or apply_ofIsComplex was also used for some results. This PR attempts to fix this confusion using the following convention:

• If the fact that the infinite place is real or complex comes from an additional hypothesis, use apply_of_isReal/apply_of_isComplex
• If the fact that the infinite place is real or complex comes from a subtype, use apply_isReal / apply_isComplex