Structures · Category theory
CategoryTheory.RingObj
A ring object in a cartesian monoidal category is an object that is equipped with an additive group structure and a (multiplicative) monoid structure that is left and right distributive over the additive structure.
- Defined in
- Mathlib.CategoryTheory.Monoidal.Ring
- Shape
- One type argument · adds mul_add, add_mul
Extends3
Extended by1
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 by11
- CategoryTheory.Hom.ring
- CategoryTheory.yonedaRingObj
- CategoryTheory.RingObj.add_mul
- CategoryTheory.RingObj.mul_add
- CategoryTheory.RingObj.toIsCommAddMonObj
- CategoryTheory.RingObj.toAddGrpObj
- CategoryTheory.Hom.add_mul
- CategoryTheory.RingObj.toMonObj
- CategoryTheory.yonedaRingObj_obj
- CategoryTheory.yonedaRingObj_map_apply
- CategoryTheory.Hom.mul_add