Commit 2023-07-26 10:47 36dc67fa

fix: redefine semiring instance on tensor product (#6141) By providing the Mul instance up front, this seems to make future typeclass search much easier. This comes at the expense of causing minor elaboration problem in various tensor definitions, which now require the implicit type arguments to be provided explicitly. This also simplifies some proofs, removing a porting note.