Theorem uniform_continuous_npow_on_bounded

Modification history

2025-01-04 14:04
Mathlib/Algebra/Order/Field/Basic.lean
chore: make uniqueness of conditionally complete linearly ordered archimedean fields independent of the construction of `Real` (#20242) …
Added uniform_continuous_npow_on_boundedView on Github →