Commit 2022-06-23 16:23 44d3fc00

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.