apply_toDual_symm_apply — Mathlib

English

If B is a nondegenerate bilinear form on V, then the map B.toDual hB: V → V* is an isomorphism, so for every f ∈ V*, v ∈ V we have B((B.toDual hB)^{-1} f, v) = f(v).

Русский

Если B — невырожденная билинейная форма на V, тогда отображение B.toDual hB: V → V* является изоморфизмом; следовательно, для каждого функционала f ∈ V*, и каждого вектора v ∈ V выполняется B((B.toDual hB)^{-1} f, v) = f(v).

LaTeX

$$$B\\left((B.toDual hB)^{-1} f, v\\right) = f(v) \\quad \\text{for all } f \\in V^*, v\\in V.$$$

Lean4

@[simp]
theorem apply_toDual_symm_apply {B : BilinForm K V} {hB : B.Nondegenerate} (f : Module.Dual K V) (v : V) :
    B ((B.toDual hB).symm f) v = f v :=
  by
  change B.toDual hB ((B.toDual hB).symm f) v = f v
  simp only [LinearEquiv.apply_symm_apply]

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