English
For any B, basis b, and vectors x,y, B(x,y) equals the dot product of the coordinate vectors with the matrix of B in the basis, applied to the coordinate representation of the other vector.
Русский
Для любой билинейной формы B, базиса b и векторов x,y, B(x,y) равно скалярному произведению координат x и y с матрицей B в этом базисе, примененного к координатам другого векторa.
LaTeX
$$B x y = (b.repr x) ⬝ᵥ (BilinForm.toMatrix b B) *ᵥ (b.repr y)$$
Lean4
theorem apply_eq_dotProduct_toMatrix_mulVec (B : BilinForm R₁ M₁) (x y : M₁) :
B x y = (b.repr x) ⬝ᵥ (BilinForm.toMatrix b B) *ᵥ (b.repr y) :=
by
nth_rw 1 [← b.sum_repr x, ← b.sum_repr y]
suffices ∑ j, ∑ i, b.repr y j * b.repr x i * B (b i) (b j) = ∑ i, ∑ j, b.repr x i * b.repr y j * B (b i) (b j) by
simpa [dotProduct, Matrix.mulVec_eq_sum, Finset.mul_sum, -Basis.sum_repr, ← mul_assoc]
simp_rw [mul_comm (b.repr y _)]
exact Finset.sum_comm
