Commit 2024-08-27 15:47 8bda9a03

View on Github →

feat: ExistsAddOfLE lemmas (#13950) Add a few convenient versions of le_iff_exists_add. From LeanAPAP

Estimated changes

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

added theorem exists_one_le_mul_of_le

modified theorem exists_one_lt_mul_of_lt'

added theorem le_iff_exists_one_le_mul

added theorem lt_iff_exists_one_lt_mul

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

deleted theorem le_iff_exists_nonneg_add

Modified Mathlib/Data/Int/Star.lean

Modified Mathlib/Data/Rat/Star.lean