toMatrix_unitsSMul — Mathlib

English

The basis constructed from unit scalars yields a diagonal matrix with the units along the diagonal.

Русский

Базис, построенный через единичные множители, задаёт диагональную матрицу со значениями на диагонали.

LaTeX

$$e.toMatrix (e.unitsSMul w) = diagonal (Function.comp Units.val w)$$

Lean4

/-- The basis constructed by `unitsSMul` has vectors given by a diagonal matrix. -/
@[simp]
theorem toMatrix_unitsSMul [DecidableEq ι] (e : Basis ι R₂ M₂) (w : ι → R₂ˣ) :
    e.toMatrix (e.unitsSMul w) = diagonal ((↑) ∘ w) := by
  ext i j
  by_cases h : i = j <;> simp [h, toMatrix_apply, unitsSMul_apply, Units.smul_def]

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