Category instances for semiring, ring, comm_semiring, and comm_ring.

We introduce the bundled categories:

Implementation notes

See the note [locally reducible category instances].

SemiRing

The category of semirings.

SemiRing.of

Construct a bundled SemiRing from the underlying type and typeclass.

Ring

The category of rings.

Ring.of

Construct a bundled Ring from the underlying type and typeclass.

CommSemiRing

The category of commutative semirings.

CommSemiRing.of

Construct a bundled CommSemiRing from the underlying type and typeclass.

CommSemiRing.has_forget_to_CommMon

The forgetful functor from commutative rings to (multiplicative) commutative monoids.

CommRing

The category of commutative rings.

CommRing.of

Construct a bundled CommRing from the underlying type and typeclass.

CommRing.has_forget_to_CommSemiRing

The forgetful functor from commutative rings to (multiplicative) commutative monoids.