Theorems · Inductive type · field theory
NormedDivisionRing
Type u_5 → Type u_5
A normed division ring is a division ring endowed with a seminorm which satisfies the equality
‖x y‖ = ‖x‖ ‖y‖.
- Defined in
- Mathlib.Analysis.Normed.Field.Basic
- Cited by
- 360 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 by377
Results whose statement or proof uses this declaration.
- norm_invstatement and proof · cited by 126
- NumberField.placestatement and proof · cited by 71
- norm_divstatement and proof · cited by 53
- intervalIntegral.integral_const_mulstatement and proof · cited by 29
- MeasureTheory.integral_smulstatement and proof · cited by 23
- norm_zpowstatement and proof · cited by 18
- HasDerivAt.div_conststatement and proof · cited by 18
- nnnorm_invstatement and proof · cited by 14
- AnalyticAt.invstatement and proof · cited by 13
- SeminormFamily.moduleFilterBasisstatement and proof · cited by 10
- intervalIntegral.integral_smulstatement and proof · cited by 10
- nhds_basis_balancedstatement and proof · cited by 10
Showing the 200 most cited of 377.