entryLinearMap — Mathlib

English

The composition of the evaluation map with the diagonal additive monoid hom equals the (i,i)-entry AddMonoidHom.

Русский

Составление evalAddMonoidHom с diagAddMonoidHom даёт (i,i)-вход AddMonoidHom.

LaTeX

$$(Pi.evalAddMonoidHom _ i).comp (diagAddMonoidHom m α) = entryAddMonoidHom α i i$$

Lean4

/-- Extracting entries from a matrix as a linear map. Note this cannot be upgraded to an algebra
homomorphism, as it does not respect multiplication.
-/
@[simps]
def entryLinearMap (i : m) (j : n) : Matrix m n α →ₗ[R] α
    where
  toFun M := M i j
  map_add' _ _ := rfl
  map_smul' _ _ := rfl

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