mult_eq

Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex

URI: https://scilib.ai/kg/mathlib#NumberField.IsTotallyComplex.mult_eq

English

In a totally complex field, every infinite place has multiplicity 2.

Русский

В полностью комплексном поле каждая бесконечная место имеет кратность 2.

LaTeX

$$$\text{IsTotallyComplex}(K) \Rightarrow \forall w \in \mathrm{InfinitePlace}(K),\ mult(w) = 2$$$

Lean4

@[simp]
theorem mult_eq [IsTotallyComplex K] (w : InfinitePlace K) : mult w = 2 :=
  mult_isComplex ⟨w, isComplex w⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru