addCommMonoid — Mathlib

English

The type of linear maps M →ₛₗ[σ₁₂] M₂ is an additive commutative monoid under pointwise addition.

Русский

Тип линейных отображений M →ₛₗ[σ₁₂] M₂ образует аддитивный коммутативный моноид по точечной сумме.

LaTeX

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

Lean4

/-- The type of linear maps is an additive monoid. -/
instance addCommMonoid : AddCommMonoid (M →ₛₗ[σ₁₂] M₂) :=
  DFunLike.coe_injective.addCommMonoid _ rfl (fun _ _ ↦ rfl) fun _ _ ↦ rfl

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