Commit 2022-11-06 02:20 f8f8be9a
View on Github →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.
- depends on: #17350