Theorem exists_pow_lt

Modification history

2026-04-11 09:33
Mathlib/Algebra/Order/Archimedean/Basic.lean
chore: move `Archimedean` to a new `Defs` file (#33894) …
Modified exists_pow_ltView on Github →
2025-07-11 09:29
Mathlib/Algebra/Order/Archimedean/Basic.lean
feat(Valued/WithZeroMulInt): generalize to any mul-archimedean Valued (#26887) …
Added exists_pow_ltView on Github →