toPreInner' — Mathlib

English

The inner product on F associated to a PreInnerProductSpace.Core structure is given by toPreInner'.inner.

Русский

Внутреннее произведение на F определяется через toPreInner'.inner.

LaTeX

$$$\\text{toPreInner'.inner}: F \\times F \\to \\mathbb{R}$$$

Lean4

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

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