English
Let B be a bilinear form on M with basis b. For x = sum_i xi b_i and y = sum_j yj b_j, we have B(x, y) = sum_i sum_j xi yj B(b_i, b_j).
Русский
Пусть B — билинейная форма на пространстве M с базисом b. Запишем x = ∑i xi b_i и y = ∑j yj b_j; тогда B(x, y) = ∑i ∑j xi yj B(b_i, b_j).
LaTeX
$$$ B(x,y) = \\sum_i \\sum_j \\xi_i \\eta_j \\ B(b_i,b_j) $, where $x = \\sum_i \\xi_i b_i$ and $y = \\sum_j \\eta_j b_j$$$
Lean4
/-- Write out `B x y` as a sum over `B (b i) (b j)` if `b` is a basis. -/
theorem sum_repr_mul_repr_mul (x y : M) :
((b.repr x).sum fun i xi => (b.repr y).sum fun j yj => xi • yj • B (b i) (b j)) = B x y :=
by
conv_rhs => rw [← b.linearCombination_repr x, ← b.linearCombination_repr y]
simp_rw [Finsupp.linearCombination_apply, Finsupp.sum, sum_left, sum_right, smul_left, smul_right, smul_eq_mul]
