toLinearMap₂'_apply' — Mathlib

English

The explicit formula for the action of Matrix.toLinearMap₂' on basis vectors matches the dot-product expression.

Русский

Явное выражение действия Matrix.toLinearMap₂' на базисные векторы совпадает с выражением через скалярное произведение.

LaTeX

$$$\text{Matrix.toLinearMap₂' }(M)(e_i,e_j) = M_{ij}$$$

Lean4

theorem toLinearMap₂'_apply' {T : Type*} [CommSemiring T] (M : Matrix n m T) (v : n → T) (w : m → T) :
    Matrix.toLinearMap₂' T M v w = v ⬝ᵥ (M *ᵥ w) :=
  by
  simp_rw [Matrix.toLinearMap₂'_apply, dotProduct, Matrix.mulVec, dotProduct]
  refine Finset.sum_congr rfl fun _ _ => ?_
  rw [Finset.mul_sum]
  refine Finset.sum_congr rfl fun _ _ => ?_
  rw [smul_eq_mul, smul_eq_mul, mul_comm (w _), ← mul_assoc]

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