mathlib

f8f8be9a - chore(algebra/order/field): split out file about powers (#17352)

chore(algebra/order/field): split out file about powers (#17352) This just pulls some material about powers of elements in linearly ordered fields into a separate file, as it isn't on the critical path to `linear_ordered_field ℚ`. This will break in CI a few times as I find the downstream imports that need it. - [x] depends on: #17350 [](https://gitpod.io/from-referrer/) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>