Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-14 10:58 38eb719f

View on Github →

feat(data/matrix/notation): relax typeclass assumptions (#11429)

Estimated changes

Modified src/data/matrix/notation.lean

modified theorem matrix.smul_vec2

modified theorem matrix.smul_vec3

Modified src/linear_algebra/cross_product.lean