diagLinearMap — Mathlib

English

The diagonal map is a linear map from n → α to Matrix n n α; i.e., it is R-linear when R is a semiring with α an AddCommMonoid module.

Русский

Диагональное отображение является линейным отображением от n → α к Matrix n n α.

LaTeX

$$$\\text{diagLinearMap}: (n \\to α) \\toₗ[R] Matrix\\ n\\ n\\ α$$$

Lean4

/-- `Matrix.diag` as a `LinearMap`. -/
@[simps]
def diagLinearMap [Semiring R] [AddCommMonoid α] [Module R α] : Matrix n n α →ₗ[R] n → α :=
  { diagAddMonoidHom n α with map_smul' := diag_smul }

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