diagonal_toLin' — Mathlib

English

The linear map given by a diagonal matrix is the direct sum of scalar multiples of projection maps; i.e., toLin'(diag(w)) equals the pi-map with w_i on the i-th projection.

Русский

Линейное отображение, задаваемое диагональной матрицей, является прямой суммой скалярных кратностей проекций; то есть toLin'(diag(w)) равно отображению, сопоставляющему каждому i множитель w_i на проекцию i.

LaTeX

$$toLin'(diagonal w) = LinearMap.pi (fun i => w i • LinearMap.proj i)$$

Lean4

theorem diagonal_toLin' (w : n → R) : toLin' (diagonal w) = LinearMap.pi fun i => w i • LinearMap.proj i :=
  LinearMap.ext fun _ => funext fun _ => mulVec_diagonal _ _ _

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