mathlib

9503f733 - feat(linear_algebra/dual): dual of a finite free module is finite free (#13896)