Commit 2023-01-28 21:03 b42511c5

View on Github →

feat: port Algebra.Module.ULift (#1880)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Module/ULift.lean

added def ULift.moduleEquiv

added theorem ULift.smul_def

Modified Mathlib/Data/ULift.lean

added theorem ULift.ext