mathlib3

029b2587 - chore(linear_algebra/tensor_product): Actually relax the requirements for add_comm_group (#5315)

chore(linear_algebra/tensor_product): Actually relax the requirements for add_comm_group (#5315) A previous commit (#5305) changed the definition to not need these, but forgot to actually change these.