Mathlib Map

Structures · Lean core

Lean.Grind.CommRing

A commutative ring, i.e. a ring with commutative multiplication.

Defined in
Init.Grind.Ring.Basic
Shape
One type argument · adds mul_comm
Open in Mathlib docs

Extends2

Extended by2

Forgetful instances

Provided automatically by

Concrete types that are instances15

  • Int
  • BitVec
  • UInt64
  • UInt8
  • UInt16
  • UInt32
  • USize
  • Int32
  • Int8
  • Int64
  • Int16
  • ISize
  • Dyadic
  • Lean.Grind.Ring.OfSemiring.Q
  • Fin

How is a type an instance?

Loading the hierarchy index…

Assumed by0

No theorem or definition in Mathlib takes this class as a hypothesis.

Ancestors24