bilinFormOfRealInner — Mathlib

English

The real inner product defines a bilinear form on F.

Русский

Действительно, вещественное внутреннее произведение определяет билинейную форму на F.

LaTeX

$$$ bilinFormOfRealInner : BilinForm_{\mathbb{R}} F $$$

Lean4

/-- The real inner product as a bilinear form.

Note that unlike `sesqFormOfInner`, this does not reverse the order of the arguments. -/
@[simps!]
def bilinFormOfRealInner : BilinForm ℝ F :=
  sesqFormOfInner.flip

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