mathlib3
13e18cfa - chore(algebra/ring/ulift): Split off and golf field instances (#18590)

Commit
2 years ago
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.
Author
Parents
Loading