Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-07 19:53 1cd74b11

View on Github →

fix(linear_algebra/finite_dimensional): universe generalize cardinal_mk_le_findim_of_linear_independent (#3721)

Estimated changes

added theorem {m}