Commit 2024-08-27 00:13 f1c03341

View on Github →

feat(Algebra/Order/Archimedean): multiplicativize Archimedean (#15589) This allows one to talk about finding powers greater than some element for ordered monoids. Before, this was only available for ordered semirings. This is to later install the instance on valuation groups (LinearOrderedCommGroupWithZero). Install the instance on NNRat and NNReal (though they are ordered semirings). Also, add some missing instances about the nonnegative submonoid.

Estimated changes

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

added theorem existsUnique_add_zpow_mem_Ioc

deleted theorem existsUnique_add_zsmul_mem_Ico

deleted theorem existsUnique_add_zsmul_mem_Ioc

added theorem existsUnique_div_zpow_mem_Ico

added theorem existsUnique_mul_zpow_mem_Ico

added theorem existsUnique_sub_zpow_mem_Ioc

deleted theorem existsUnique_sub_zsmul_mem_Ico

deleted theorem existsUnique_sub_zsmul_mem_Ioc

added theorem existsUnique_zpow_near_of_one_lt'

added theorem existsUnique_zpow_near_of_one_lt

deleted theorem existsUnique_zsmul_near_of_pos'

deleted theorem existsUnique_zsmul_near_of_pos

deleted theorem exists_lt_nsmul

added theorem exists_lt_pow

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

Modified Mathlib/Data/NNReal/Basic.lean