mathlib

44d3fc00 - chore(data/nat,int): move field-specific lemmas about cast (#14890)

chore(data/nat,int): move field-specific lemmas about cast (#14890) I want to refer to the rational numbers in the definition of a field, meaning we can't have `algebra.field.basic` in the transitive imports of `data.rat.basic`. This is a step in rearranging those imports: remove the definition of a field from the dependencies of the casts `ℕ → α` and `ℤ → α`, where `α` is a (semi)ring.