Theorem exists_pow_lt₀

Modification history

2025-07-11 09:29
Mathlib/GroupTheory/ArchimedeanDensely.lean
feat(Valued/WithZeroMulInt): generalize to any mul-archimedean Valued (#26887) …
Added exists_pow_lt₀View on Github →