Structures · Lean core
Lean.Grind.AddCommMonoid
A type with zero and addition, where addition is commutative and associative, and the zero is the right identity for addition.
- Defined in
- Init.Grind.Module.Basic
- Shape
- One type argument · adds add_zero, add_comm, add_assoc
Extends2
Extended by2
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.