Commit 2019-11-19 11:07 e3be70db
View on Github →lemmas about powers of elements (#1688)
- feat(algebra/archimedean): add alternative version of exists_int_pow_near
- also add docstrings
- feat(analysis/normed_space/basic): additional inequality lemmas
- that there exists elements with large and small norms in a nondiscrete normed field.
- doc(algebra/archimedean): edit docstrings
- Apply suggestions from code review Co-Authored-By: Chris Hughes 33847686+ChrisHughes24@users.noreply.github.com