instAddCommGroup — Mathlib

Lean4
instance : AddCommGroup (Poly α) where
  add := ((· + ·) : Poly α → Poly α → Poly α)
  neg := (Neg.neg : Poly α → Poly α)
  sub := Sub.sub
  zero := 0
  nsmul := @nsmulRec _ ⟨(0 : Poly α)⟩ ⟨(· + ·)⟩
  zsmul := @zsmulRec _ ⟨(0 : Poly α)⟩ ⟨(· + ·)⟩ ⟨Neg.neg⟩ (@nsmulRec _ ⟨(0 : Poly α)⟩ ⟨(· + ·)⟩)
  add_zero _ := by ext; simp_rw [add_apply, zero_apply, add_zero]
  zero_add _ := by ext; simp_rw [add_apply, zero_apply, zero_add]
  add_comm _ _ := by ext; simp_rw [add_apply, add_comm]
  add_assoc _ _ _ := by ext; simp_rw [add_apply, ← add_assoc]
  neg_add_cancel _ := by ext; simp_rw [add_apply, neg_apply, neg_add_cancel, zero_apply]
Похожие утверждения