Commit 2024-03-19 22:00 d0257020

View on Github →

chore: Move pow_lt_pow_succ to Algebra.Order.WithZero (#11507) These lemmas can be defined earlier, ridding us of an import in Algebra.GroupPower.Order

Estimated changes

Modified Mathlib/Algebra/GroupPower/Order.lean

deleted theorem pow_lt_pow_right₀

deleted theorem pow_lt_pow_succ

deleted theorem pow_pos_iff

Modified Mathlib/Algebra/Order/Field/Basic.lean

Modified Mathlib/Algebra/Order/Floor.lean

modified theorem Nat.ceil_eq_zero

Modified Mathlib/Algebra/Order/WithZero.lean

added theorem pow_lt_pow_right₀

added theorem pow_lt_pow_succ

added theorem pow_pos_iff

Modified Mathlib/Data/Ordmap/Ordset.lean

Modified Mathlib/Order/RelSeries.lean