Commit 2025-04-12 16:30 53c7c8fa

View on Github →

chore(Archimedean/Basic): rename type variables (#23834)

Estimated changes

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

modified theorem add_one_pow_unbounded_of_pos

modified theorem archimedean_iff_int_le

modified theorem archimedean_iff_int_lt

modified theorem archimedean_iff_nat_le

modified theorem archimedean_iff_nat_lt

modified theorem archimedean_iff_rat_le

modified theorem archimedean_iff_rat_lt

modified theorem eq_of_forall_rat_lt_iff_lt

modified theorem existsUnique_add_zpow_mem_Ioc

modified theorem existsUnique_div_zpow_mem_Ico

modified theorem existsUnique_mul_zpow_mem_Ico

modified theorem existsUnique_sub_zpow_mem_Ioc

modified theorem existsUnique_zpow_near_of_one_lt'

modified theorem existsUnique_zpow_near_of_one_lt

modified theorem exists_floor

modified theorem exists_int_gt

modified theorem exists_int_lt

modified theorem exists_nat_ge

modified theorem exists_nat_gt

modified theorem exists_nat_one_div_lt

modified theorem exists_pos_rat_lt

modified theorem exists_pow_btwn

modified theorem exists_pow_btwn_of_lt_mul

modified theorem exists_rat_btwn

modified theorem exists_rat_gt

modified theorem exists_rat_lt

modified theorem exists_rat_near

modified theorem exists_rat_pow_btwn

modified theorem exists_zpow_btwn_of_lt_mul

modified theorem le_iff_forall_rat_lt_imp_le

modified theorem le_of_forall_rat_lt_imp_le

modified theorem pow_unbounded_of_one_lt

Modified Mathlib/Data/NNReal/Defs.lean