instCStarRingReal — Mathlib

English

The real numbers form a C*-ring with the usual absolute value as a norm; hence norm_mul_self_le holds in ℝ with star being the identity.

Русский

Числа ℝ образуют C*-кольцо, норму задаёт обычное абсолютное значение; поэтому неравенство norm_mul_self_le выполняется в ℝ, где звезда — тождественная операция.

LaTeX

$$$\mathbb{R} \text{ is a } C^*\text{-ring with the usual norm } \|x\| = |x|.$$$

Lean4

instance : CStarRing ℝ where
  norm_mul_self_le x := by simp only [Real.norm_eq_abs, abs_mul_abs_self, star, id, norm_mul, le_refl]

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