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





leanprover-community/mathlib,leanprover-community/mathlib