English
Let B be a bilinear form on a vector space V over a field K, and let b be a left-separating element for B (i.e., B is nondegenerate on the left). Then the natural map m ↦ (n ↦ B(m,n)) realizes B via its associated dual form, so for all m,n ∈ V we have (B.toDual b)(m)(n) = B(m,n).
Русский
Пусть B — билинейная форма на векторном пространстве V над полем K, и пусть b является элементом слева, обеспечивающим развёрнутость B (то есть B невырождена слева). Тогда естественное отображение m ↦ (n ↦ B(m,n)) реализует B через ассоциированную двойственную форму, следовательно для всех m, n ∈ V выполняется (B.toDual b)(m)(n) = B(m,n).
LaTeX
$$$\\forall m,n \\in V,\\quad (B.toDual hB)(m)(n) = B(m,n).$$$
Lean4
theorem toDual_def {B : BilinForm K V} (b : B.SeparatingLeft) {m n : V} : B.toDual b m n = B m n :=
rfl
