English
For bilinear maps, the evaluation B x y can be computed as a double sum over basis coordinates of x and y.
Русский
Для билинейных отображений B вычисление B x y выполняется как двойная сумма по координатам базиса x и y.
LaTeX
$$$\\displaystyle ((b_1.repr x).sum\\ i\\; (b_2.repr y).sum\\ j\\; i \\; j \\; B (b_1 i) (b_2 j)) = B x y$$$
Lean4
/-- Write out `B x y` as a sum over `B (b i) (b j)` if `b` is a basis.
Version for bilinear maps, see `sum_repr_mul_repr_mulₛₗ` for the semi-bilinear version. -/
theorem sum_repr_mul_repr_mul {B : Mₗ →ₗ[Rₗ] Nₗ →ₗ[Rₗ] Pₗ} (x y) :
((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, map_sum₂, map_sum, LinearMap.map_smul₂, LinearMap.map_smul]
