Commit 2024-05-15 20:27 4417a5a6

View on Github →

feat(Topology/Algebra/NormedValued): add correspondence (#12432) Nontrivial nonarchimedean norms correspond to rank one valuations.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Real/Basic.lean

added def IsNonarchimedean

Modified Mathlib/Data/Real/NNReal.lean

added theorem NNReal.exists_lt_of_strictMono

added theorem Real.exists_lt_of_strictMono

Created Mathlib/Topology/Algebra/NormedValued.lean

added def NormedField.toValued

added def NormedField.valuation

added theorem NormedField.valuation_apply

added def Valued.norm

added theorem Valued.norm_add_le

added theorem Valued.norm_eq_zero

added theorem Valued.norm_nonneg

added def Valued.toNormedField