mathlib
38642efc - chore(data/rat): rename `data.rat.basic` to `data.rat.defs` (#14895)

Commit
3 years ago
chore(data/rat): rename `data.rat.basic` to `data.rat.defs` (#14895) This is a preparatory step for PR #14893 that moves only the `field ℚ` instance (and its small set of dependencies) back to `data.rat.basic`; doing this in two moves should produce a neater set of diffs.
Author
Parents
Loading