Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-24 13:55 b9bf921c

View on Github →

chore(linear_algebra): switch to named constructors for linear_map (#8059) This makes some ideas I have for future refactors easier, and generally makes things less fragile to changes such as additional fields or reordering of fields. The extra verbosity is not really significant. This conversion is not exhaustive, there may be anonymous constructors elsewhere that I've missed.

Estimated changes