mathlib3

ef0ef216 - chore(algebra/order/field): don't import finiteness hierarchy (#17350)

chore(algebra/order/field): don't import finiteness hierarchy (#17350) This problem was just introduced in #16971. Hopefully we can all be careful about not adding heavy imports to fundamental files. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>