Mathlib v3 is deprecated. Go to Mathlib v4

Def ulift.ring_equiv

Modification history

2021-06-07 15:40
src/algebra/ring/ulift.lean
feat(algebra/ring/basic): define non-unital, non-associative rings (#6786) …
Modified ulift.ring_equivView on Github →
2020-08-05 11:37
src/algebra/ring/ulift.lean
feat(algebra/*/ulift): algebraic instances for ulift (#3675)
Added ulift.ring_equivView on Github →