Structures · Lean core
Lean.Grind.Semiring
A semiring, i.e. a type equipped with addition, multiplication, and a map from the natural numbers,
satisfying appropriate compatibilities.
Use Ring instead if the type also has negation,
CommSemiring if the multiplication is commutative,
or CommRing if the type has negation and multiplication is commutative.
- Defined in
- Init.Grind.Ring.Basic
- Shape
- One type argument · adds natCast, ofNat, nsmul, npow, add_zero, add_comm, add_assoc, mul_assoc, mul_one, one_mul, left_distrib, right_distrib, zero_mul, mul_zero, pow_zero, pow_succ, ofNat_succ, ofNat_eq_natCast, nsmul_eq_natCast_mul
Extends2
Extended by3
Forgetful instances
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by0
No theorem or definition in Mathlib takes this class as a hypothesis.