indexRealUnits — Mathlib

English

The index RealUnits K is either 1 or 2, depending on CM-field specifics; the exact value is controlled by a two-case criterion.

Русский

Индекс RealUnits(K) равен 1 или 2; конкретное значение определяется двумя случаями в зависимости от CM-поля.

LaTeX

$$$$ \\operatorname{indexRealUnits}(K) = 1 \\;\\lor\\; \\operatorname{indexRealUnits}(K) = 2 $$$$

Lean4

/-- The index of the subgroup of `(𝓞 K)ˣ` generated by the real units and the roots of unity. This
index is equal to `1` or `2`, see `indexRealUnits_eq_one_or_two` and `indexRealUnits_eq_two_iff`.
-/
noncomputable abbrev indexRealUnits : ℕ :=
  (realUnits K ⊔ torsion K).index

Похожие утверждения