Mathlib v3 is deprecated. Go to Mathlib v4

Theorem norm_one

Modification history

2019-10-08 15:54

src/analysis/normed_space/basic.lean

chore(analysis): put lemmas in normed_field namespace (#1517) …

Deleted norm_one View on Github →

2018-10-02 14:08

analysis/normed_space.lean

feat(data/padics): prove Hensel's lemma

Modified norm_one View on Github →

2018-10-02 14:02

analysis/normed_space.lean

feat(data/padics): use has_norm typeclasses for padics

Added norm_one View on Github →