mathlib

b4979cbd - chore(data/rat): split `field ℚ` instance from definition of `ℚ` (#14893)

chore(data/rat): split `field ℚ` instance from definition of `ℚ` (#14893) I want to refer to the rational numbers in the definition of a field, meaning we can't define the field structure on `ℚ` in the same file as `ℚ` itself. This PR moves everything in `data/rat/basic.lean` that does not depend on `algebra/field/basic.lean` into a new file `data/rat/defs.lean`: definition of the type `ℚ`, the operations giving its algebraic structure, and the coercions from integers and natural numbers. Basically, everything except the actual `field ℚ` instance. It turns out our basic lemmas on rational numbers only require a `comm_ring`, `comm_group_with_zero` and `is_domain` instance, so I defined those instances in `defs.lean` could leave all lemmas intact. As a consequence, the transitive imports provided by `data.rat.basic` are somewhat smaller: no `linear_ordered_field` is needed until `data.rat.order`. I see this as a bonus but can also re-import `algebra.order.field` in `data.rat.basic` if desired.