instAddCommGroup — Mathlib

English

The space α →ᵇ β is equipped with an AddCommGroup structure compatible with the pointwise operations and the coercion map.

Русский

Пространство α →ᵇ β наделено структурой AddCommGroup, совместимой с точечно-скалярными операциями и тождественным отображением.

LaTeX

$$$\text{AddCommGroup}(\alpha \to^b \beta)$ with coordinatewise operations$$

Lean4

instance instAddCommGroup : AddCommGroup (α →ᵇ β) :=
  fast_instance%DFunLike.coe_injective.addCommGroup _ coe_zero coe_add coe_neg coe_sub (fun _ _ => coe_nsmul _ _)
      fun _ _ => coe_zsmul _ _

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