Theorem ULift.rat_cast_down

Modification history

2023-03-17 15:06
Mathlib/Algebra/Ring/ULift.lean
chore: Split off and golf `ulift` field instances (#2911) …
Deleted ULift.rat_cast_downView on Github →
2023-01-04 15:31
Mathlib/Algebra/Ring/ULift.lean
chore: rename HasRatCast to RatCast (#1329)
Modified ULift.rat_cast_downView on Github →
2022-12-28 14:53
Mathlib/Algebra/Ring/ULift.lean
feat: port Algebra.Ring.Ulift (#1240) …
Added ULift.rat_cast_downView on Github →