Commit 2023-12-15 20:19 e609a7ec

View on Github →

refactor: Generalise archimedean lemmas to semirings (#8943) A bunch of lemmas are true in ℕ but previously did not apply there.

Estimated changes

Modified Mathlib/Algebra/Order/Archimedean.lean

modified theorem add_one_pow_unbounded_of_pos

modified theorem exists_nat_gt

modified theorem exists_nat_one_div_lt

modified theorem exists_nat_pow_near

modified theorem pow_unbounded_of_one_lt