toBilin'_apply — Mathlib

English

The coefficient of a matrix in the bilinear form basis expansion equals the sum of products of coordinates of x, M, and y.

Русский

Коэффициент матрицы в базисной раскладке билинейной формы равен сумме произведений координат x, M и y.

LaTeX

$$$\text{toBilin'}(M)\;x\;y = \sum_i \sum_j x_i M_{ij} y_j$$$

Lean4

theorem toBilin'_apply (M : Matrix n n R₁) (x y : n → R₁) : Matrix.toBilin' M x y = ∑ i, ∑ j, x i * M i j * y j :=
  (Matrix.toLinearMap₂'_apply _ _ _).trans (by simp only [smul_eq_mul, mul_comm, mul_left_comm])

Похожие утверждения