Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-05 11:37 4a82e849

View on Github →

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

Estimated changes

Created src/algebra/group/ulift.lean

added theorem ulift.inv_down

added theorem ulift.mul_down

added def ulift.mul_equiv

added theorem ulift.one_down

added theorem ulift.sub_down

Modified src/algebra/module/pi.lean

Created src/algebra/module/ulift.lean

added def ulift.semimodule_equiv

added theorem ulift.smul_down'

added theorem ulift.smul_down

Created src/algebra/ring/ulift.lean

added def ulift.ring_equiv