Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ring_equiv.Pi_congr_right_refl

Modification history

2022-04-26 07:55
src/algebra/ring/equiv.lean
feat(algebra/ring/equiv): generalize `ring_equiv` material to allow for non-unital rings (#13626)
Modified ring_equiv.Pi_congr_right_reflView on Github →
2022-02-28 10:33
src/data/equiv/ring.lean
feat(algebra/algebra,data/equiv/ring): `{ring,alg}_equiv.Pi_congr_right` (#12289) …
Added ring_equiv.Pi_congr_right_reflView on Github →