mathlib
d1b2d6eb - fix(linear_algebra/tensor_algebra): Correct the precedence of `⊗ₜ[R]` (#5619)

Commit
5 years ago
fix(linear_algebra/tensor_algebra): Correct the precedence of `⊗ₜ[R]` (#5619) Previously, `a ⊗ₜ[R] b = c` was interpreted as `a ⊗ₜ[R] (b = c)` which was nonsense because `eq` is not in `Type`. I'm not sure whether `:0` is necessary, but it seems harmless. The `:100` is the crucial bugfix here.
Author
Parents
Loading