toInner' — Mathlib

English

The inner product is defined by the core as ⟪x,y⟫ = (cd.inner 𝕜 x y).

Русский

Скалярное произведение задаётся ядром как ⟪x,y⟫ = cd.inner 𝕜 x y.

LaTeX

$$$\langle x,y\rangle_{cd} = \langle x,y\rangle$$$

Lean4

/-- Inner product defined by the `InnerProductSpace.Core` structure. We can't reuse
`InnerProductSpace.Core.toInner` because it takes `InnerProductSpace.Core` as an explicit
argument. -/
def toInner' : Inner 𝕜 F :=
  cd.toInner

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