Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ulift.one_down

Modification history

2020-08-05 11:37

src/algebra/group/ulift.lean

feat(algebra/*/ulift): algebraic instances for ulift (#3675)

Added ulift.one_down View on Github →