instAddCommMonoid — Mathlib

English

The set of polynomial laws M →ₚₗ[R] N carries the structure of an AddCommMonoid under pointwise addition.

Русский

Множество полиномальных законов имеет структуру AddCommMonoid под точечно заданным сложением.

LaTeX

$$$(\operatorname{PolynomialLaw}(R,M,N), +, 0) \text{ is an AddCommMonoid}$.$$

Lean4

instance : AddCommMonoid (M →ₚₗ[R] N)
    where
  add_assoc f g h := by ext; simp only [add_def, add_assoc]
  zero_add f := by ext; simp only [add_def, zero_add, zero_def]
  add_zero f := by ext; simp only [add_def, add_zero, zero_def]
  nsmul n f := (n : R) • f
  nsmul_zero f := by simp only [Nat.cast_zero, zero_smul f]
  nsmul_succ n f := by simp only [Nat.cast_add, Nat.cast_one, add_smul, one_smul]
  add_comm f g := by ext; simp only [add_def, add_comm]

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