Mathlib v3 is deprecated. Go to Mathlib v4

Def mul_equiv.Pi_congr_right

Modification history

2021-05-06 22:46

src/data/equiv/mul_add.lean

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

Added mul_equiv.Pi_congr_right View on Github →