Commit 2024-10-25 14:17 27e4d0a1

View on Github →

feat(Topology/Algebra/Valued/NormedValued): add lemmas for Valued.toNormedField (#16758) Add simp lemmas for Valued.toNormedField. Prove isNonarchimedean for this norm. Add definition Valued.toNontriviallyNormedField.

Estimated changes

Modified Mathlib/Topology/Algebra/Valued/NormedValued.lean

added def Valued.toNontriviallyNormedField:

added theorem Valued.toNormedField.norm_le_iff

added theorem Valued.toNormedField.norm_le_one_iff

added theorem Valued.toNormedField.norm_lt_iff

added theorem Valued.toNormedField.norm_lt_one_iff

added theorem Valued.toNormedField.one_le_norm_iff

added theorem Valued.toNormedField.one_lt_norm_iff