Structures · Algebra
RingInvoClass
RingInvoClass F R states that F is a type of ring involutions.
You should extend this class when you extend RingInvo.
- Defined in
- Mathlib.RingTheory.RingInvo
- Shape
- 2 explicit arguments · adds involution
Extends1
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- RingInvo
How is a type an instance?
Loading the hierarchy index…