Def IsNonarchimedean

Modification history

2024-07-30 11:18

Mathlib/Data/Real/Basic.lean

feat(Analysis.Normed.Ring.SeminormFromConst): add seminormFromConst (#14361) …

Modified IsNonarchimedean View on Github →

2024-05-15 20:27

Mathlib/Data/Real/Basic.lean

feat(Topology/Algebra/NormedValued): add correspondence (#12432) …

Added IsNonarchimedean View on Github →