Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-02 10:55 d6a7c3bc

View on Github →

chore(algebra/algebra/basic): add alg_hom.of_linear_map and lemmas (#8151) This lets me golf complex.lift a little

Estimated changes