Structures · Analysis
NormedDivisionRing
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
- Shape
- One type argument · adds dist_eq, norm_mul
Extends3
Extended by1
Forgetful instances
Concrete types that are instances1
- Quaternion
How is a type an instance?
Loading the hierarchy index…
Assumed by383
- norm_inv
- NumberField.place
- norm_div
- intervalIntegral.integral_const_mul
- MeasureTheory.integral_smul
- norm_zpow
- HasDerivAt.div_const
- nnnorm_inv
- AnalyticAt.inv
- nhds_basis_balanced
- intervalIntegral.integral_smul
- SeminormFamily.moduleFilterBasis
- LinearMap.extendOfNorm
- Polynomial.cauchyBound
- DifferentiableAt.div_const
- DifferentiableAt.inv
- AnalyticAt.zpow
- LinearEquiv.extend
- LinearMap.extendOfNorm_eq
- Asymptotics.isLittleO_iff_tendsto'
- differentiableAt_inv
- Asymptotics.IsLittleO.tendsto_div_nhds_zero
- enorm_inv
- deriv_div_const
- Asymptotics.isLittleO_of_tendsto'
- Balanced.smul_mono
- Filter.tendsto_inv₀_cobounded
- tsum_geometric_of_norm_lt_one
- Differentiable.div_const
- AnalyticAt.zpow_nonneg
- deriv_const_mul_field
- deriv_const_mul_field'
- Bornology.IsVonNBounded.image
- Asymptotics.isLittleO_of_tendsto
- Seminorm.smul_ball_zero
- NormedSpace.expSeries_div_hasSum_exp
- uniqueDiffWithinAt_iff_accPt
- MeasureTheory.integrable_smul_iff
- Asymptotics.isLittleO_iff_tendsto
- DifferentiableAt.fun_inv
- DilationEquiv.smulTorsor
- Asymptotics.isLittleO_pow_pow
- DifferentiableWithinAt.inv
- Seminorm.absorbent_ball_zero
- Asymptotics.IsLittleO.inv_rev
- Asymptotics.IsBigO.smul
- egauge_zero_right
- MeasureTheory.eLpNorm_const_smul
- AnalyticWithinAt.inv
- MeasureTheory.Integrable.div_const
Ancestors125
- Add
- AddAction
- AddCancelCommMonoid
- AddCancelMonoid
- AddCommGroup
- AddCommGroupWithOne
- AddCommMagma
- AddCommMonoid
- AddCommMonoidWithOne
- AddCommSemigroup
- AddGroup
- AddGroupWithOne
- AddLeftCancelMonoid
- AddLeftCancelSemigroup
- AddMonoid
- AddMonoidWithOne
- AddRightCancelMonoid
- AddRightCancelSemigroup
- AddSemigroup
- AddSemigroupAction
- AddTorsor
- AddZero
- AddZeroClass
- AlgebraicGeometry.QuasiSeparated
- Bornology
- Bracket
- ChartedSpace
- CompactSpace
- CompactlyCoherentSpace
- Dist
- Distrib
- Div
- DivInvMonoid
- DivInvOneMonoid
- DivisionMonoid
- DivisionRing
- DivisionSemiring
- Dvd
- EDist
- EMetricSpace
- ENorm
- GroupWithZero
- HAdd
- HDiv
- HMul
- HSMul
- HSub
- HVAdd
- IntCast
- Inv
- InvOneClass
- InvolutiveInv
- InvolutiveNeg
- IsLeftCancelAdd
- IsRightCancelAdd
- IsSemiprimaryRing
- Lean.Grind.AddCommGroup
- Lean.Grind.AddCommMonoid
- Lean.Grind.IntModule
- Lean.Grind.NatModule
- Lean.Grind.Ring
- Lean.Grind.Semiring
- LocallyPathConnectedSpace
- MetricSpace
- Monoid
- MonoidWithZero
- Mul
- MulAction
- MulOne
- MulOneClass
- MulZeroClass
- MulZeroOneClass
- NNDist
- NNNorm
- NNRatCast
- NPow
- NSMul
- NatCast
- Neg
- NegZeroClass
- NonAssocRing
- NonAssocSemiring
- NonUnitalNonAssocRing
- NonUnitalNonAssocSemiring
- NonUnitalNormedRing
- NonUnitalRing
- NonUnitalSeminormedRing
- NonUnitalSemiring
- Nonempty
- Nontrivial
- Norm
- NormedAddCommGroup
- NormedAddGroup
- NormedRing
- OfNat
- OfScientific
- One
- PrespectralSpace
- PseudoEMetricSpace
- PseudoMetricSpace
- QuasiSeparatedSpace
- RatCast
- Ring
- SMul
- Semigroup
- SemigroupAction
- SemigroupWithZero
- SeminormedAddCommGroup
- SeminormedAddGroup
- SeminormedRing
- Semiring
- SequentialSpace
- Sub
- SubNegMonoid
- SubNegZeroMonoid
- SubtractionCommMonoid
- SubtractionMonoid
- TopologicalSpace
- Topology.IsGeneratedBy
- UniformSpace
- VAdd
- VSub
- ZPow
- ZSMul
- Zero