Theorem free_abelian_group.to_add_comm_group.ext

style(linear_algebra/tensor_product): rename of -> tmul and ⊗ₛ -> ⊗ₜ; some cleanup in free_abelian_group

feat(linear_algebra,group_theory): add tensor product and supporting material