mathlib3

a33315d5 - feat(linear_algebra/dim): findim equivalence (#1217)

feat(linear_algebra/dim): findim equivalence (#1217) * feat(linear_algebra/dim): findim equivalence * feat(linear_algebra/dim): two versions of dim_fun * feat(linear_algebra/dim): clean up