mathlib3

8817c3ea - chore(linear_algebra/tensor_product): Relax the ring requirement to semiring for the group instance (#5305)