Mathlib v3 is deprecated. Go to Mathlib v4

Def ring_equiv.Pi_congr_right

Modification history

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_rightView on Github →