instNormedField — Mathlib

English

The complex numbers form a normed field with the usual absolute value as the norm and complex multiplication as the product.

Русский

Комплексные числа образуют нормированное поле с обычной нормой |·| и умножением как произведением.

LaTeX

$$$ \\mathbb{C} \text{ is a NormedField with the usual norm and multiplication }$$$

Lean4

instance : NormedField ℂ where
  dist_eq _ _ := rfl
  norm_mul := Complex.norm_mul

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