Theorems · Inductive type · functional analysis
NormedRing
Type u_5 → Type u_5
A normed ring is a ring endowed with a norm which satisfies the inequality ‖x y‖ ≤ ‖x‖ ‖y‖.
- Defined in
- Mathlib.Analysis.Normed.Ring.Basic
- Cited by
- 924 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,014
Results whose statement or proof uses this declaration.
- HasSummableGeomSeriesstatement · cited by 60
- MeasureTheory.Integrable.const_mulstatement and proof · cited by 58
- Asymptotics.IsBigO.mulstatement and proof · cited by 29
- MeasureTheory.Lp.simpleFunc.modulestatement and proof · cited by 29
- NormedSpace.expSeries_radius_eq_topstatement and proof · cited by 27
- HasDerivAt.const_mulstatement and proof · cited by 25
- ContinuousMap.toLpstatement and proof · cited by 21
- HasDerivAt.mulstatement and proof · cited by 20
- selfAdjoint.expUnitarystatement and proof · cited by 19
- AnalyticAt.smulstatement and proof · cited by 18
- CFC.logstatement and proof · cited by 17
- MeasureTheory.Integrable.mul_conststatement and proof · cited by 17
Showing the 200 most cited of 1,014.