English
For CM-field K, the number of infinite places of K and its maximal real subfield K⁺ are related by a quadratic extension, yielding equality of certain counts of real/complex places.
Русский
Для CM‑поля K количество бесконечных мест и его максимального вещественного подполя K⁺ взаимосвязано через квадратичное разложение, приводя к равенству некоторых характеристик реальных/комплексных мест.
LaTeX
$$$\\text{card}(\\text{InfinitePlace } K^+) = \\text{card}(\\text{InfinitePlace } K).$$$
Lean4
@[macro _private.Mathlib.NumberTheory.NumberField.CMField.0.NumberField.IsCMField.«termK⁺»]
public meta def
«_aux_Mathlib_NumberTheory_NumberField_CMField___macroRules__private_Mathlib_NumberTheory_NumberField_CMField_0_NumberField_IsCMField_termK⁺_1» :
Macro✝ := fun
| `(K⁺) => `(maximalRealSubfield K)
| _ => no_error_if_unused% throw✝ Lean.Macro.Exception.unsupportedSyntax✝
