Theorem ULift.int_cast_down

Modification history

2023-03-17 15:06
Mathlib/Algebra/Group/ULift.lean
chore: Split off and golf `ulift` field instances (#2911) …
Deleted ULift.int_cast_downView on Github →
2022-12-08 06:45
Mathlib/Algebra/Group/ULift.lean
feat: port algebra.group.ulift (#906) …
Added ULift.int_cast_downView on Github →