English
Write out B x y for semi-bilinear B as a double sum over i and j using the representations of x and y in the bases.
Русский
Записать B x y как двойную сумму по i, j через представления x и y в базисах.
LaTeX
$$$\\displaystyle (b_1'.repr\\ x).sum\\ i\\; (b_2'.repr\\ y).sum\\ j\\; ρ_{12}i \\; σ_{12}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 semi-bilinear maps, see `sum_repr_mul_repr_mul` for the bilinear version. -/
theorem sum_repr_mul_repr_mulₛₗ {B : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] 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ₛₗ]
