Structures · Lean core
Lean.Grind.Ring
A ring, i.e. a type equipped with addition, negation, multiplication, and a map from the integers,
satisfying appropriate compatibilities.
Use CommRing if the multiplication is commutative.
- Defined in
- Init.Grind.Ring.Basic
- Shape
- One type argument · adds intCast, zsmul, neg_add_cancel, sub_eq_add_neg, neg_zsmul, zsmul_natCast_eq_nsmul, intCast_ofNat, intCast_neg
Extends3
Extended by2
Forgetful instances
Every Lean.Grind.Ring is also a
Provided automatically by
Concrete types that are instances1
- Lean.Grind.Ring.OfSemiring.Q
How is a type an instance?
Loading the hierarchy index…
Assumed by0
No theorem or definition in Mathlib takes this class as a hypothesis.