Commit 2025-04-15 16:20 bc0f16d2

View on Github →

chore(Archimedean/Basic): minor cleanup (#23854)

Estimated changes

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

modified theorem exists_lt_pow

modified theorem exists_nat_ge