English
The set of polynomial laws from M to N over R carries an additive commutative group structure under pointwise addition; the zero element is the zero map, and addition is defined pointwise.
Русский
Множество полиномальных законов из M в N над R оборудовано аддитивной коммутативной группой под покомпонентным сложением; нулевым элементом является нулевая карта, сложение задаётся по каждому аргументу.
LaTeX
$$$\\{ f: M \\to_{R} N \\mid f \\text{ is a polynomial law over } R \\}$ is an AddCommGroup with $(f+g)(m)=f(m)+g(m)$ and $0(m)=0$.$$
Lean4
instance : AddCommGroup (M →ₚₗ[R] N) where
zsmul n f := (n : R) • f
zsmul_zero' f := by simp only [Int.cast_zero, zero_smul]
zsmul_succ' n
f := by simp only [Nat.cast_succ, Int.cast_add, Int.cast_natCast, Int.cast_one, add_smul, _root_.one_smul]
zsmul_neg' n
f := by
ext S _ _ m
rw [neg_def]
simp only [Int.cast_negSucc, Nat.cast_add, Nat.cast_one, neg_add_rev, _root_.add_smul, add_def_apply,
smul_def_apply, Nat.succ_eq_add_one, Int.cast_add, Int.cast_natCast, Int.cast_one, _root_.one_smul, add_def,
smul_def, Pi.smul_apply, Pi.add_apply, smul_add, smul_smul, neg_mul, one_mul]
rw [add_comm]
neg_add_cancel
f := by
ext S _ _ m
simp only [add_def_apply, neg_def, Pi.smul_apply, zero_def, Pi.zero_apply]
nth_rewrite 2 [← _root_.one_smul (M := R) (b := f.toFun' S m)]
rw [← _root_.add_smul]
simp only [neg_add_cancel, _root_.zero_smul]
add_comm f g := by ext; simp only [add_def, add_comm]
