basic): Rename `pow_minus_two_nonneg` (#18591)

Commit

2 years ago

chore(algebra/order/field/basic): Rename `pow_minus_two_nonneg` (#18591) Rename `pow_minus_two_nonneg` to `zpow_neg_two_nonneg` and move it to `algebra.order.field.power`.

Author

YaelDillies

Parents

eea141bc

mathlib3 acb3d204 - chore(algebra/order/field/basic): Rename `pow_minus_two_nonneg` (#18591)

mathlib3
acb3d204 - chore(algebra/order/field/basic): Rename `pow_minus_two_nonneg` (#18591)