Commit 2025-08-31 17:16 4a2cfa25
View on Github →chore(RingTheory/TensorProduct/Basic): generalize result (#29158)
Generalize TensorProduct.Algebra.mul'_comp_tensorTensorTensorComm to use NonUnitalNonAssocSemiring instead of Semiring and add LinearMap.mul'_tensor (moved these down so that we can use the variables instead of reintroducing the same variables).