Commit 2022-06-27 16:25 68e01601
View on Github →chore(data/int/cast): redo #14890, moving field-specific lemmas (#14995)
In #14894, 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.defs.
Apparently this dependency was re-added, so I'm going to have to split it again...