Structures · Analysis

NormedCommGroup

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

Open in Mathlib docs

Extends3

Extended by0

Nothing extends this class yet.

Forgetful instances

Every NormedCommGroup is also a

Concrete types that are instances7

SeparationQuotient
Subtype
Prod
OrderDual
ULift
HasQuotient.Quotient
Multiplicative

How is a type an instance?

Loading the hierarchy index…