Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-22 04:38 9485a857

View on Github →

fix(linear_algebra/basic): make R explicit in linear_equiv.refl (#2161)

  • fix(linear_algebra/basic): make R explicit in linear_equiv.refl
  • getting mathlib to compile again
  • better variablism

Estimated changes