Structures · Algebra
StarRingEquivClass
StarRingEquivClass F A B asserts F is a type of bundled ⋆-ring equivalences between A and
B.
You should also extend this typeclass when you extend StarRingEquiv.
- Defined in
- Mathlib.Algebra.Star.StarRingHom
- Shape
- 3 explicit arguments · adds map_star
Extends1
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- StarAlgEquiv
- StarRingEquiv
How is a type an instance?
Loading the hierarchy index…