Theorems · Inductive type · field theory
NormedField
Type u_5 → Type u_5
A normed field is a field with a norm satisfying ‖x y‖ = ‖x‖ ‖y‖.
- Defined in
- Mathlib.Analysis.Normed.Field.Basic
- Cited by
- 1,084 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 by1,349
Results whose statement or proof uses this declaration.
- NormedSpacestatement · cited by 12,499
- NormedAlgebrastatement · cited by 1,165
- AffineIsometryEquivstatement · cited by 118
- IsRCLikeNormedFieldstatement · cited by 104
- AffineIsometrystatement · cited by 79
- WithSeminormsstatement · cited by 69
- StrictConvexSpacestatement · cited by 57
- ZSpan.fundamentalDomainstatement and proof · cited by 48
- UniformConvergenceCLMstatement and proof · cited by 44
- AffineIsometry.toAffineMapstatement and proof · cited by 42
- NormedSpace.restrictScalarsstatement and proof · cited by 39
- norm_algebraMap'statement and proof · cited by 39
Showing the 200 most cited of 1,349.