Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-05 16:28 8e79ea53

View on Github →

feat(data/matrix/basic): add alg_(hom|equiv).map_matrix (#8527) This also adds a few standalone lemmas about algebra_map.

Estimated changes