toBilin_apply — Mathlib

English

The product of the matrix of B with M and N equals the matrix of B composed with the corresponding linear maps.

Русский

Произведение матрицы B на M и N равно матрице билинейной формы, полученной композицией с соответствующими линейными отображениями.

LaTeX

$$M * B.toMatrix' * N = (B.comp (M^T).toLin' N.toLin').toMatrix'$$

Lean4

@[simp]
theorem toBilin_apply (M : Matrix n n R₁) (x y : M₁) :
    Matrix.toBilin b M x y = ∑ i, ∑ j, b.repr x i * M i j * b.repr y j :=
  (Matrix.toLinearMap₂_apply _ _ _ _ _).trans
    (by simp only [smul_eq_mul, mul_comm, mul_left_comm])
      -- Not a `simp` lemma since `BilinForm.toMatrix` needs an extra argument

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