Structures · Lean core
Lean.Grind.AddCommGroup
A type with zero, addition, negation, and subtraction, where addition is commutative and associative, and negation is the left inverse of addition.
- Defined in
- Init.Grind.Module.Basic
- Shape
- One type argument · adds neg_add_cancel, sub_eq_add_neg
Extends3
Extended by2
Forgetful instances
Provided automatically by
Concrete types that are instances1
- Vector
How is a type an instance?
Loading the hierarchy index…
Assumed by0
No theorem or definition in Mathlib takes this class as a hypothesis.