instAddCommGroup — Mathlib

English

The space of continuous affine maps is an additive commutative group under pointwise operations.

Русский

Пространство непрерывных аффинных отображений образует коммутативную группу сложения, по точкам.

LaTeX

$$$\text{AddCommGroup}(\,P \toᴬ[R] W\,)$$$

Lean4

instance : AddCommGroup (P →ᴬ[R] W) :=
  coe_injective.addCommGroup _ coe_zero coe_add coe_neg coe_sub (fun _ _ ↦ coe_smul _ _) fun _ _ ↦ coe_smul _ _

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