Mathlib Map

Structures · Analysis

NormedAddCommGroup

A normed group is an additive 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
Open in Mathlib docs

Extends3

Extended by1

Forgetful instances

Every NormedAddCommGroup is also a

Provided automatically by

Concrete types that are instances41

  • Int
  • Real
  • Rat
  • Complex
  • SeparationQuotient
  • ContinuousLinearMap
  • BoundedContinuousFunction
  • CStarMatrix
  • UniformSpace.Completion
  • TensorProduct
  • Quaternion
  • WithLp
  • TrivSqZeroExt
  • RestrictScalars
  • ContinuousMapZero
  • ZeroAtInftyContinuousMap
  • ContinuousAlternatingMap
  • WithCStarModule
  • ContinuousMultilinearMap
  • Hamming
  • AddCircle
  • ContinuousAffineMap
  • PiLp
  • NormedAddGroupHom
  • Real.Angle
  • Manifold.IsSubmersionAt.complement
  • Manifold.IsImmersionAt.complement
  • Manifold.IsSubmersionAtOfComplement.smallComplement
  • Manifold.IsImmersion.complement
  • Manifold.IsImmersionAtOfComplement.smallComplement
  • Manifold.IsSubmersion.complement
  • Subtype
  • Prod
  • OrderDual
  • ULift
  • MulOpposite
  • PUnit
  • HasQuotient.Quotient
  • ContinuousMap
  • Shrink
  • Additive

How is a type an instance?

Loading the hierarchy index…

Assumed by17,124

Ancestors69