English
The product a·M_{i j}·star b equals the inner product between (equiv...).symm applied to Pi.single j b and the operator toCLM M applied to Pi.single i a, establishing the compatibility of matrix multiplication with the inner product.
Русский
Произведение a · M_{i j} · star(b) равно скалярному произведению между соответствующим вектором и образующей линейного отображения toCLM M, показывая совместимость умножения матрицы и скалярного произведения.
LaTeX
$$$a \cdot M_{i j} \cdot \star b = \langle (\text{equiv}).symm (\Pi.single j b),\; toCLM M (\text{equiv}).symm (\Pi.single i a) \rangle_A$$$
Lean4
theorem mul_entry_mul_eq_inner_toCLM [Fintype n] [DecidableEq m] [DecidableEq n] {M : CStarMatrix m n A} {i : m} {j : n}
(a b : A) :
a * M i j * star b = ⟪equiv _ _ |>.symm (Pi.single j b), toCLM M (equiv _ _ |>.symm <| Pi.single i a)⟫_A := by
simp [mul_assoc, inner_def]
