Commit 2025-04-11 08:18 5dfc3a98

View on Github →

feat(Order/GroupWithZero): drop more TC assumptions (#23922) Prove PosMulReflectLT.toPosMulStrictMono and use it as a local instance to drop even more TC assumptions. This is a follow-up to #23892 and #23901.

Estimated changes

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

modified theorem Finset.mul₀_sup'

modified theorem Finset.sup'_div₀

modified theorem Finset.sup'_mul₀

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

added theorem MulPosReflectLT.toMulPosStrictMono

added theorem PosMulReflectLT.toPosMulStrictMono

added theorem Right.inv_pos

modified theorem div_nonneg

modified theorem div_pos

modified theorem zpow_nonneg

modified theorem zpow_pos

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

added theorem PosMulMono.toMulPosMono

added theorem PosMulReflectLE.toMulPosReflectLE

added theorem PosMulReflectLT.toMulPosReflectLT

added theorem PosMulStrictMono.toMulPosStrictMono

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

modified def OrderIso.divRight₀