Structures · Lean core
Lean.Grind.CommSemiring
A commutative semiring, i.e. a semiring with commutative multiplication.
Use CommRing if the type has negation.
- Defined in
- Init.Grind.Ring.Basic
- Shape
- One type argument · adds mul_comm
Extends1
Extended by2
Forgetful instances
Provided automatically by
Concrete types that are instances1
- Nat
How is a type an instance?
Loading the hierarchy index…
Assumed by0
No theorem or definition in Mathlib takes this class as a hypothesis.