mathlib

41556652 - refactor(linear_algebra/dual): replace dim<omega by finite_dimensional (#5775)