instAddCommGroup — Mathlib

Lean4

/-- `RatFunc K` is an additive commutative group.

This is an intermediate step on the way to the full instance `RatFunc.instCommRing`.
-/
def instAddCommGroup : AddCommGroup (RatFunc K) where
  add := (· + ·)
  add_assoc := by frac_tac
  add_comm := by frac_tac
  zero := 0
  zero_add := by frac_tac
  add_zero := by frac_tac
  neg := Neg.neg
  neg_add_cancel := by frac_tac
  sub := Sub.sub
  sub_eq_add_neg := by frac_tac
  nsmul := (· • ·)
  nsmul_zero := by smul_tac
  nsmul_succ _ := by smul_tac
  zsmul := (· • ·)
  zsmul_zero' := by smul_tac
  zsmul_succ' _ := by smul_tac
  zsmul_neg' _ := by smul_tac

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