Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-20 11:23 ed8d597a

View on Github →

fix(data/matrix/basic): remove an accidental requirement for a matrix to be square (#8372)

Estimated changes

modified theorem matrix.mul_apply'