Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-03-17 00:32 13e18cfa

View on Github →

chore(algebra/ring/ulift): Split off and golf field instances (#18590) Move field-like instances on ulift from algebra.ring.ulift to a new file algebra.field.ulift. Golf them by declaring the has_nat_cast and has_int_cast instances earlier.

Estimated changes