Description: A normed ring is a ring with an induced topology and metric such that the metric is translation-invariant and the norm (distance from 0) is an absolute value on the ring. (Contributed by Mario Carneiro, 4-Oct-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | df-nrg |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cnrg | ||
1 | vw | ||
2 | cngp | ||
3 | cnm | ||
4 | 1 | cv | |
5 | 4 3 | cfv | |
6 | cabv | ||
7 | 4 6 | cfv | |
8 | 5 7 | wcel | |
9 | 8 1 2 | crab | |
10 | 0 9 | wceq |