instCoreOfCore — Mathlib

English

Given an InnerProductSpace.Core data on F, the inner product is defined by this core structure.

Русский

Дано данные Core для внутреннего произведения, тогда само скалярное произведение задаётся этой структурой ядра.

LaTeX

$$$\\text{InnerProductSpace.Core.toPreInner'} : \\text{Inner } \\mathbb{𝕜} F$$$

Lean4

instance (𝕜 : Type*) (F : Type*) [RCLike 𝕜] [AddCommGroup F] [Module 𝕜 F] [cd : InnerProductSpace.Core 𝕜 F] :
    PreInnerProductSpace.Core 𝕜 F where
  inner := cd.inner
  conj_inner_symm := cd.conj_inner_symm
  re_inner_nonneg := cd.re_inner_nonneg
  add_left := cd.add_left
  smul_left := cd.smul_left

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