toInnerProductSpaceable_ofReal — Mathlib

English

If E is a normed real space, then InnerProductSpaceable E; i.e., the real case yields an inner product.

Русский

В случае вещественного поля 𝕜 = ℝ нормированное пространство E обладает внутренним произведением.

LaTeX

$$$\text{InnerProductSpaceable } E$$$

Lean4

instance (priority := 100) toInnerProductSpaceable_ofReal [InnerProductSpace ℝ E] : InnerProductSpaceable E :=
  ⟨parallelogram_law_with_norm ℝ⟩

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