Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-06 22:46 48bdd1e3

View on Github →

feat(data/equiv,linear_algebra): Pi_congr_right for mul_equiv and linear_equiv (#7489) This PR generalizes equiv.Pi_congr_right to linear equivs, adding the mul_equiv/add_equiv version as well. To be used in the bundled-basis refactor

Estimated changes