English
The dot product of x with the matrix of B sandwiched between the coordinate representations of y equals B applied to the basis coordinates of x and y.
Русский
Скалярное произведение x и матрица B в сочетании с координатами x и y в базисе равно B(x,y).
LaTeX
$$x ⬝ᵥ (BilinForm.toMatrix b B) *ᵥ y = B (b.equivFun.symm x) (b.equivFun.symm y)$$
Lean4
theorem dotProduct_toMatrix_mulVec (B : BilinForm R₁ M₁) (x y : n → R₁) :
x ⬝ᵥ (BilinForm.toMatrix b B) *ᵥ y = B (b.equivFun.symm x) (b.equivFun.symm y) :=
by
simp only [dotProduct, mulVec_eq_sum, op_smul_eq_smul, Finset.sum_apply, Pi.smul_apply, transpose_apply,
toMatrix_apply, smul_eq_mul, mul_sum, Basis.equivFun_symm_apply, map_sum, map_smul, coeFn_sum, LinearMap.smul_apply]
rw [Finset.sum_comm]
refine Finset.sum_congr rfl (fun i _ ↦ Finset.sum_congr rfl fun j _ ↦ ?_)
ring
