normAtPlace_real — Mathlib

English

The normAtPlace evaluated at a purely real-valued vector (c,c) equals |c|.

Русский

Норма на месте для вектора (c,c) равна |c|.

LaTeX

$$$\operatorname{normAtPlace}(w)((\lambda\,\_, \lambda\,\_)) = |\!c\!|.$$$

Lean4

theorem normAtPlace_real (w : InfinitePlace K) (c : ℝ) :
    normAtPlace w ((fun _ ↦ c, fun _ ↦ c) : (mixedSpace K)) = |c| := by
  rw [show ((fun _ ↦ c, fun _ ↦ c) : (mixedSpace K)) = c • 1 by ext <;> simp, normAtPlace_smul, map_one, mul_one]

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