Commit 2022-06-23 16:23 44d3fc00
View on Github →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.