instNormedAddCommGroup — Mathlib

English

The complex numbers form a Normed Additive Commutative Group with the standard norm, defined by ‖z‖ = √(normSq z).

Русский

Комплексные числа образуют нормированную аддитивную коммутативную группу со стандартной нормой, заданной ‖z‖ = √(normSq z).

LaTeX

$$$\forall z \in \mathbb{C},\; \|z\| = \sqrt{\operatorname{normSq}(z)}$$$

Lean4

instance instNormedAddCommGroup : NormedAddCommGroup ℂ :=
  AddGroupNorm.toNormedAddCommGroup
    { toFun := norm
      map_zero' := norm_map_zero'
      add_le' := norm_add_le'
      neg' := norm_neg'
      eq_zero_of_map_eq_zero' := fun _ ↦ norm_eq_zero_iff.mp }

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