mult_isReal — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem mult_isReal (w : { w : InfinitePlace K // IsReal w }) : mult w.1 = 1 := by rw [mult, if_pos w.prop]

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