Commit 2023-01-10 21:45 daa535fc

View on Github →

feat: port Algebra.Order.Archimedean (#1462)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Hom/Equiv/Basic.lean

Created Mathlib/Algebra/Order/Archimedean.lean

added theorem add_one_pow_unbounded_of_pos

added theorem archimedean_iff_int_le

added theorem archimedean_iff_int_lt

added theorem archimedean_iff_nat_le

added theorem archimedean_iff_nat_lt

added theorem archimedean_iff_rat_le

added theorem archimedean_iff_rat_lt

added theorem eq_of_forall_lt_rat_iff_lt

added theorem eq_of_forall_rat_lt_iff_lt

added theorem existsUnique_add_zsmul_mem_Ico

added theorem existsUnique_add_zsmul_mem_Ioc

added theorem existsUnique_zsmul_near_of_pos'

added theorem existsUnique_zsmul_near_of_pos

added theorem exists_floor

added theorem exists_int_gt

added theorem exists_int_lt

added theorem exists_mem_Ico_zpow

added theorem exists_mem_Ioc_zpow

added theorem exists_nat_ge

added theorem exists_nat_gt

added theorem exists_nat_one_div_lt

added theorem exists_nat_pow_near

added theorem exists_nat_pow_near_of_lt_one

added theorem exists_pos_rat_lt

added theorem exists_pow_lt_of_lt_one

added theorem exists_rat_btwn

added theorem exists_rat_gt

added theorem exists_rat_lt

added theorem exists_rat_near

added theorem le_of_forall_lt_rat_imp_le

added theorem le_of_forall_rat_lt_imp_le

added theorem pow_unbounded_of_one_lt