mathlib

48bdd1e3 - feat(data/equiv,linear_algebra): `Pi_congr_right` for `mul_equiv` and `linear_equiv` (#7489)

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 Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>