Commit 2025-01-04 14:04 464a3677

View on Github →

chore: make uniqueness of conditionally complete linearly ordered archimedean fields independent of the construction of Real (#20242) Also avoid one import of Analysis/ in Algebra/.

Estimated changes

Modified Mathlib.lean

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

added theorem exists_pow_btwn

modified theorem exists_rat_gt

added theorem exists_rat_pow_btwn

Modified Mathlib/Algebra/Order/CompleteField.lean

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

added theorem uniform_continuous_npow_on_bounded

Modified Mathlib/Algebra/Order/Ring/Abs.lean

added theorem abs_pow_sub_pow_le

Modified Mathlib/Analysis/SpecialFunctions/Pow/Real.lean

deleted theorem Real.exists_rat_pow_btwn

deleted theorem Real.exists_rat_pow_btwn_rat

deleted theorem Real.exists_rat_pow_btwn_rat_aux

Created Mathlib/Data/Real/CompleteField.lean