Commit 2025-07-07 17:19 2d0be376

View on Github →

feat: (· ^ n) is strictly monotone on nonnegative inputs for n : ℤ (#26762) This is the import-wise non-problematic part of #23177.

Estimated changes

Modified Mathlib/Algebra/GroupWithZero/WithZero.lean

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

deleted theorem one_lt_zpow

Modified Mathlib/Algebra/Order/GroupWithZero/Unbundled/Basic.lean

added theorem div_lt_one₀

added theorem one_lt_div₀

added theorem zpow_left_strictMonoOn₀

Modified Mathlib/Algebra/Order/Monoid/Unbundled/Pow.lean

added theorem one_lt_zpow