Structures · Analysis
NormedField
A normed field is a field with a norm satisfying ‖x y‖ = ‖x‖ ‖y‖.
- Defined in
- Mathlib.Analysis.Normed.Field.Basic
- Shape
- One type argument · adds dist_eq, norm_mul
Extends3
Extended by2
Forgetful instances
Every NormedField is also a
Concrete types that are instances11
- Real
- Rat
- Complex
- Padic
- UniformSpace.Completion
- PadicComplex
- IsDedekindDomain.HeightOneSpectrum.adicCompletion
- PadicAlgCl
- NumberField.InfinitePlace.Completion
- Subtype
- WithAbs
How is a type an instance?
Loading the hierarchy index…
Assumed by1,467
- ZSpan.fundamentalDomain
- UniformConvergenceCLM
- AffineIsometry.toAffineMap
- norm_algebraMap'
- NormedSpace.restrictScalars
- spectralRadius
- Module.Basis.ofZLatticeBasis
- normSeminorm
- spectralNorm
- IsRCLikeNormedField.rclike
- AffineIsometryEquiv.symm
- AffineIsometry.injective
- ContinuousLinearMap.toLinearMap₁₂
- IsConformalMap
- PointwiseConvergenceCLM
- AffineIsometryEquiv.toAffineEquiv
- AffineSubspace.subtypeₐᵢ
- ContinuousLinearMap.postcomp
- absorbent_nhds_zero
- SchwartzMap.seminorm
- ContinuousLinearEquiv.arrowCongr
- ZLattice.comap
- NormedField.toValued
- AffineIsometryEquiv.pointReflection
- AffineIsometry.coe_toAffineMap
- ZSpan.fract
- CompactConvergenceCLM
- ContinuousLinearMap.precomp
- ContinuousMultilinearMap.compContinuousLinearMapL
- AffineIsometry.linearIsometry
- AffineIsometry.isometry
- ContinuousAlternatingMap.apply
- ContinuousMultilinearMap.apply
- ContinuousAlternatingMap.compContinuousLinearMapCLM
- norm_withSeminorms
- Module.Basis.ofZLatticeBasis_apply
- AffineIsometryEquiv.toAffineIsometry
- spectrum.norm_le_norm_of_mem
- WithSeminorms.topologicalAddGroup
- ContinuousLinearMapWOT.comp
- AffineIsometryEquiv.refl
- ContinuousLinearEquiv.conjContinuousAlgEquiv
- ZSpan.floor
- Module.Basis.norm
- ContinuousLinearMap.toBilinForm
- AffineIsometryEquiv.isometry
- AffineIsometryEquiv.toContinuousAffineEquiv
- AffineIsometryEquiv.trans
- PiTensorProduct.projectiveSeminormAux
- spectralAlgNorm
Ancestors154
- 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
- CommGroupWithZero
- CommMagma
- CommMonoid
- CommMonoidWithZero
- CommRing
- CommSemigroup
- CommSemiring
- CompactSpace
- CompactlyCoherentSpace
- Dist
- Distrib
- Div
- DivInvMonoid
- DivInvOneMonoid
- DivisionCommMonoid
- DivisionMonoid
- DivisionRing
- DivisionSemiring
- Dvd
- EDist
- EMetricSpace
- ENorm
- EuclideanDomain
- Field
- GroupWithZero
- HAdd
- HDiv
- HMod
- HMul
- HSMul
- HSub
- HVAdd
- Ideal.FiniteHeight
- IntCast
- Inv
- InvOneClass
- InvolutiveInv
- InvolutiveNeg
- IsJacobsonRing
- IsLeftCancelAdd
- IsRightCancelAdd
- IsSemiprimaryRing
- Lean.Grind.AddCommGroup
- Lean.Grind.AddCommMonoid
- Lean.Grind.CommRing
- Lean.Grind.CommSemiring
- Lean.Grind.Field
- Lean.Grind.IntModule
- Lean.Grind.NatModule
- Lean.Grind.Ring
- Lean.Grind.Semiring
- LocallyPathConnectedSpace
- MetricSpace
- Mod
- Monoid
- MonoidWithZero
- Mul
- MulAction
- MulOne
- MulOneClass
- MulZeroClass
- MulZeroOneClass
- NNDist
- NNNorm
- NNRatCast
- NPow
- NSMul
- NatCast
- Neg
- NegZeroClass
- NonAssocCommRing
- NonAssocCommSemiring
- NonAssocRing
- NonAssocSemiring
- NonUnitalCommRing
- NonUnitalCommSemiring
- NonUnitalNonAssocCommRing
- NonUnitalNonAssocCommSemiring
- NonUnitalNonAssocRing
- NonUnitalNonAssocSemiring
- NonUnitalNormedCommRing
- NonUnitalNormedRing
- NonUnitalRing
- NonUnitalSeminormedCommRing
- NonUnitalSeminormedRing
- NonUnitalSemiring
- Nonempty
- Nontrivial
- Norm
- NormedAddCommGroup
- NormedAddGroup
- NormedCommRing
- NormedDivisionRing
- NormedRing
- OfNat
- OfScientific
- One
- PrespectralSpace
- PseudoEMetricSpace
- PseudoMetricSpace
- QuasiSeparatedSpace
- RatCast
- Ring
- SMul
- Semifield
- Semigroup
- SemigroupAction
- SemigroupWithZero
- SeminormedAddCommGroup
- SeminormedAddGroup
- SeminormedCommRing
- SeminormedRing
- Semiring
- SequentialSpace
- Sub
- SubNegMonoid
- SubNegZeroMonoid
- SubtractionCommMonoid
- SubtractionMonoid
- TopologicalSpace
- Topology.IsGeneratedBy
- UniformSpace
- VAdd
- VSub
- ZPow
- ZSMul
- Zero