diagonalLinearMap — Mathlib

English

The diagonal map is linear: diagAddMonoidHom n α extends to a linear map diagLinearMap: (n → α) →ₗ[R] Matrix n n α, i.e., the diagonal map is R-linear.

Русский

Диагональное отображение является линейным отображением: diagLinearMap: (n → α) →ₗ[R] Matrix n n α.

LaTeX

$$$\\text{diagLinearMap}: (n \\to α) \\toₗ[R] Matrix\\ n\\ n\\ α$ with $\\operatorname{diagLinearMap}(v) = \\operatorname{diag}(v)$.$$

Lean4

/-- `Matrix.diagonal` as a `LinearMap`. -/
@[simps]
def diagonalLinearMap [Semiring R] [AddCommMonoid α] [Module R α] : (n → α) →ₗ[R] Matrix n n α :=
  { diagonalAddMonoidHom n α with map_smul' := diagonal_smul }

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