Structures · Analysis
NontriviallyNormedField
A nontrivially normed field is a normed field in which there is an element of norm different
from 0 and 1. This makes it possible to bring any element arbitrarily close to 0 by
multiplication by the powers of any element, and thus to relate algebra and topology.
- Defined in
- Mathlib.Analysis.Normed.Field.Basic
- Shape
- One type argument · adds non_trivial
Extends1
Extended by1
Forgetful instances
Concrete types that are instances4
- Padic
- PadicComplex
- PadicAlgCl
- Subtype
How is a type an instance?
Loading the hierarchy index…
Assumed by9,462
- modelWithCornersSelf
- deriv
- DifferentiableAt
- TangentSpace
- HasDerivAt
- DifferentiableWithinAt
- DifferentiableOn
- ModelWithCorners.prod
- fderiv
- ModelWithCorners.toFun'
- fderivWithin
- HasFDerivWithinAt
- ContDiff
- HasFDerivAt
- HasDerivWithinAt
- AnalyticAt
- extChartAt
- Differentiable
- ContDiffOn
- ContDiffWithinAt
- ContMDiff
- ContDiffAt
- HasStrictFDerivAt
- derivWithin
- iteratedFDeriv
- AnalyticOnNhd
- ContMDiffOn
- MDifferentiableAt
- ContMDiffAt
- MDifferentiableWithinAt
- ContMDiffWithinAt
- iteratedDeriv
- meromorphicOrderAt
- HasStrictDerivAt
- AnalyticOn
- MeromorphicAt
- mfderiv
- FormalMultilinearSeries.radius
- iteratedFDerivWithin
- HasDerivAt.deriv
- ModelWithCorners.symm
- MeromorphicOn
- DifferentiableAt.hasFDerivAt
- MDifferentiable
- OpenPartialHomeomorph.extend
- DifferentiableWithinAt.hasFDerivWithinAt
- ContinuousLinearMap.flip
- mfderivWithin
- ContMDiffMap
- iteratedDerivWithin
Ancestors156
- 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
- Infinite
- 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
- NormedField
- 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