Commit 2022-06-22 16:29 f57c0cdc
View on Github →chore(algebra/{group_power,order}): split off field lemmas (#14849)
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 half of rearranging those imports: remove the definition of a field from the dependencies of basic lemmas about nsmul, npow, zsmul and zpow.