Theorems · Inductive type · field theory
NontriviallyNormedField
Type u_5 → Type u_5
A nontrivially normed field is a normed field in which there is an element of norm different
from 0 and 1. This makes it possible to bring any element arbitrarily close to 0 by
multiplication by the powers of any element, and thus to relate algebra and topology.
- Defined in
- Mathlib.Analysis.Normed.Field.Basic
- Cited by
- 8,742 results in Mathlib
- Foundations
- Depth 0 from the axioms, rests on 1 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by9,588
Results whose statement or proof uses this declaration.
- ModelWithCornersstatement · cited by 2,462
- modelWithCornersSelfstatement and proof · cited by 920
- derivstatement and proof · cited by 676
- DifferentiableAtstatement and proof · cited by 617
- TangentSpacestatement and proof · cited by 555
- HasDerivAtstatement and proof · cited by 493
- DifferentiableWithinAtstatement and proof · cited by 453
- DifferentiableOnstatement and proof · cited by 419
- ModelWithCorners.prodstatement and proof · cited by 414
- fderivstatement · cited by 398
- ModelWithCorners.toFun'statement and proof · cited by 373
- fderivWithinstatement · cited by 357
Showing the 200 most cited of 9,588.