Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ring_equiv.to_equiv_commutes

Modification history

2021-03-14 03:22
src/data/equiv/ring.lean
chore(equiv/*): add missing lemmas to traverse coercion diamonds (#6648) …
Added ring_equiv.to_equiv_commutesView on Github →