Structures · Algebra
CentroidHomClass
CentroidHomClass F α states that F is a type of centroid homomorphisms.
You should extend this class when you extend CentroidHom.
- Defined in
- Mathlib.Algebra.Ring.CentroidHom
- Shape
- 2 explicit arguments · adds map_mul_left, map_mul_right
Extends1
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- CentroidHom
How is a type an instance?
Loading the hierarchy index…