Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-05 18:04 d1b2d6eb

View on Github →

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.

Estimated changes