mathlib

30553f13 - feat(algebra/hom/centroid): Introduce the centroid of a (non-unital, non-associative) semiring (#12746)

feat(algebra/hom/centroid): Introduce the centroid of a (non-unital, non-associative) semiring (#12746) Define the centroid of a (non-unital, non-associative) semiring and shows that it forms a semiring. The centroid of a (non-unital, non-associative) ring is a ring. When the ring is prime, the centroid is commutative. Co-authored-by: Yaël Dillies <yael.dillies@gmail.com> Co-authored-by: Christopher Hoskin <christopher.hoskin@gmail.com> Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com>