Commit 2025-04-10 02:58 4c17d273

View on Github →

feat(Order/GroupWithZero): drop some 0 ≤ 1 assumptions (#23892) In these lemmas, the assumptions imply 0 < 1, so we don't need to assume that.

Estimated changes

Modified Mathlib/Algebra/Order/GroupWithZero/Finset.lean

modified theorem Finset.sup'_div₀

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

modified theorem div_le_one_of_le₀

modified theorem inv_le_one_of_one_le₀

modified theorem inv_pos

modified theorem mul_inv_le_one_of_le₀

modified theorem one_le_inv_iff₀

modified theorem zpow_nonneg

modified theorem zpow_pos

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

modified def OrderIso.divRight₀

Modified Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean

Modified Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean