normAtPlace_neg — Mathlib

English

normAtPlace at w is unchanged by negating x: normAtPlace w (-x) = normAtPlace w x.

Русский

Норма на месте сохраняется при замене x на -x: ||-x||_w = ||x||_w.

LaTeX

$$$\operatorname{normAtPlace}(w)(-x) = \operatorname{normAtPlace}(w)(x).$$$

Lean4

theorem normAtPlace_neg (w : InfinitePlace K) (x : mixedSpace K) : normAtPlace w (-x) = normAtPlace w x :=
  by
  rw [normAtPlace, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk]
  split_ifs <;> simp

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