toLin'_one — Mathlib

English

A variant form showing equality between the matrix product and the application of f.

Русский

Вариант, показывающий равенство между произведением матрицы и применением f.

LaTeX

$$theorem toMatrix'_mulVec (f : LinearMap (RingHom.id R) (n → R) (m → R)) (v : n → R) : ((LinearMap.toMatrix' f).mulVec v) = f v$$

Lean4

@[simp]
theorem toLin'_one : Matrix.toLin' (1 : Matrix n n R) = LinearMap.id :=
  Matrix.mulVecLin_one

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