evalAddMonoidHom — Mathlib

English

The type of linear maps is an additive monoid under pointwise addition (and zero).

Русский

Тип линейных отображений образует аддитивный моноид по точечной сумме (и нулю).

LaTeX

$$AddCommMonoid (M →ₛₗ[σ₁₂] M₂)$$

Lean4

/-- Evaluation of a `σ₁₂`-linear map at a fixed `a`, as an `AddMonoidHom`. -/
@[simps]
def evalAddMonoidHom (a : M) : (M →ₛₗ[σ₁₂] M₂) →+ M₂
    where
  toFun f := f a
  map_add' f g := LinearMap.add_apply f g a
  map_zero' := rfl

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