Commit 2024-07-16 00:30 a5fc1b2a

View on Github →

chore (Algebra.Order.Monoid.Canonical.Defs): split off ExistsAddOfLE and ExistsMulOfLE (#14390) The type classes ExistsAddOfLE and ExistsMulOfLE are unbundled versions of canonical ordering. To use them properly and avoid bundled ordered algebraic classes, we should put them in a separate file.

Estimated changes

Modified Mathlib.lean

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

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

Modified Mathlib/Algebra/Order/Interval/Set/Monoid.lean

Modified Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean

deleted theorem exists_one_lt_mul_of_lt'

deleted theorem le_iff_forall_one_lt_lt_mul'

deleted theorem le_of_forall_one_lt_le_mul

deleted theorem le_of_forall_one_lt_lt_mul'

Created Mathlib/Algebra/Order/Monoid/Unbundled/ExistsOfLE.lean

added theorem exists_one_lt_mul_of_lt'

added theorem le_iff_forall_one_lt_lt_mul'

added theorem le_of_forall_one_lt_le_mul

added theorem le_of_forall_one_lt_lt_mul'

Modified Mathlib/Algebra/Order/Pi.lean

Modified Mathlib/Algebra/Order/Ring/Defs.lean