Mathlib v3 is deprecated. Go to Mathlib v4

Theorem mul_equiv.Pi_congr_right_refl

Modification history

2022-04-26 07:55
src/algebra/hom/equiv.lean
feat(algebra/ring/equiv): generalize `ring_equiv` material to allow for non-unital rings (#13626)
Modified mul_equiv.Pi_congr_right_reflView on Github →
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_reflView on Github →