mult_isComplex — Mathlib

English

Let w be a complex infinite place of K. Then the local multiplier is equal to 2: mult(w) = 2.

Русский

Пусть w — комплексное бесконечное место поля K. Тогда локальный множитель равен 2: mult(w) = 2.

LaTeX

$$$\forall w \in \{ w : \mathrm{InfinitePlace} K \mid \mathrm{IsComplex} w \}, \operatorname{mult}(w) = 2$$$

Lean4

@[simp]
theorem mult_isComplex (w : { w : InfinitePlace K // IsComplex w }) : mult w.1 = 2 := by
  rw [mult, if_neg (not_isReal_iff_isComplex.mpr w.prop)]

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