Commit 2023-03-16 13:33 acb3d204

View on Github →

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.

Estimated changes

Modified src/algebra/order/field/basic.lean

deleted theorem pow_minus_two_nonneg

Modified src/algebra/order/field/power.lean

added theorem zpow_neg_two_nonneg

Modified src/analysis/special_functions/bernstein.lean