Structures · Analysis
NormedGroup
A normed group is a group endowed with a norm for which dist x y = ‖x⁻¹ * y‖ defines a metric
space structure.
- Defined in
- Mathlib.Analysis.Normed.Group.Defs
- Shape
- One type argument · adds dist_eq
Extends3
Extended by1
Forgetful instances
Concrete types that are instances5
- Subtype
- Prod
- OrderDual
- ULift
- Multiplicative
How is a type an instance?
Loading the hierarchy index…
Assumed by33
- norm_eq_zero'
- norm_le_zero_iff'
- norm_div_eq_zero_iff
- norm_pos_iff'
- nnnorm_ne_zero_iff'
- eq_one_or_norm_pos
- nnnorm_eq_zero'
- normGroupNorm
- tendsto_norm_inv_mul_self_nhdsNE
- comap_norm_nhdsGT_zero'
- NormedGroup.toENormedMonoid
- NormedGroup.toSeminormedGroup
- OrderDual.normedGroup
- ULift.normedGroup
- norm_ne_zero_iff'
- eq_of_norm_div_eq_zero
- NormedGroup.dist_eq
- norm_div_pos_iff
- Pi.normedGroup
- eq_one_or_nnnorm_pos
- Subgroup.normedGroup
- NormedGroup.toGroup
- coe_normGroupNorm
- eq_of_norm_div_le_zero
- Additive.normedAddGroup
- NormedGroup.toMetricSpace
- NormedGroup.induced
- NormedGroup.toNorm
- nnnorm_pos'
- NormedCommGroup.induced
- tendsto_norm_nhdsNE_one
- Prod.normedGroup
- SubgroupClass.normedGroup
Ancestors60
- AlgebraicGeometry.QuasiSeparated
- Bornology
- CancelMonoid
- ChartedSpace
- CompactSpace
- CompactlyCoherentSpace
- Dist
- Div
- DivInvMonoid
- DivInvOneMonoid
- DivisionMonoid
- Dvd
- EDist
- EMetricSpace
- ENorm
- Group
- HDiv
- HMul
- HSMul
- Inv
- InvOneClass
- InvolutiveInv
- IsLeftCancelMul
- IsRightCancelMul
- LeftCancelMonoid
- LeftCancelSemigroup
- LocallyPathConnectedSpace
- MetricSpace
- Monoid
- Mul
- MulAction
- MulOne
- MulOneClass
- NNDist
- NNNorm
- NPow
- NSMul
- Nonempty
- Norm
- OfNat
- One
- PrespectralSpace
- PseudoEMetricSpace
- PseudoMetricSpace
- QuasiSeparatedSpace
- RightCancelMonoid
- RightCancelSemigroup
- SDiv
- SMul
- Semigroup
- SemigroupAction
- SeminormedGroup
- SequentialSpace
- TopologicalSpace
- Topology.IsGeneratedBy
- Torsor
- UniformSpace
- ZPow
- ZSMul
- Zero