innerProductSpace — Mathlib

English

An equivalent reformulation: ∥x+y∥ = ∥x∥ + ∥y∥ iff ∥y∥ x is equal to ∥x∥ y.

Русский

Эквивалентная формулировка: ∥x+y∥ = ∥x∥ + ∥y∥ тогда и только тогда, когда ∥y∥ x = ∥x∥ y.

LaTeX

$$$\|x+y\| = \|x\| + \|y\| \iff \|y\| \cdot x = \|x\| \cdot y$$$

Lean4

/-- A field `𝕜` satisfying `RCLike` is itself a `𝕜`-inner product space. -/
instance innerProductSpace : InnerProductSpace 𝕜 𝕜
    where
  inner x y := y * conj x
  norm_sq_eq_re_inner x := by simp only [mul_conj, ← ofReal_pow, ofReal_re]
  conj_inner_symm x y := by simp only [mul_comm, map_mul, starRingEnd_self_apply]
  add_left x y z := by simp only [mul_add, map_add]
  smul_left x y z := by simp only [mul_comm (conj z), mul_assoc, smul_eq_mul, map_mul]

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