Commit 2022-02-28 10:33 200c2541
View on Github →feat(algebra/algebra,data/equiv/ring): {ring,alg}_equiv.Pi_congr_right (#12289)
We extend {add,mul}_equiv.Pi_congr_right to rings and algebras.
Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/.60ring_equiv.2EPi_congr_right.60