Mathlib Map

Structures · Topology

IsTopologicalAddGroup

A topological (additive) group is a group in which the addition and negation operations are continuous. When you declare an instance that does not already have a UniformSpace instance, you should also provide an instance of UniformSpace and IsUniformAddGroup using IsTopologicalAddGroup.rightUniformSpace and isUniformAddGroup_of_addCommGroup.

Defined in
Mathlib.Topology.Algebra.Group.Defs
Shape
One type argument
Open in Mathlib docs

Extends2

Extended by3

Concrete types that are instances31

  • Real
  • Rat
  • TopCat.carrier
  • SeparationQuotient
  • ContinuousLinearMap
  • CStarMatrix
  • Matrix
  • RestrictedProduct
  • ModuleCat.carrier
  • AddUnits
  • ContinuousAlternatingMap
  • ContinuousLinearMapWOT
  • WithIdealFilter
  • ContinuousMultilinearMap
  • SchwartzMap
  • TestFunction
  • ContDiffMapSupportedIn
  • UniformConvergenceCLM
  • ContinuousAddMonoidHom
  • WeakDual
  • TangentSpace
  • WeakSpace
  • WeakBilin
  • TopRep.V
  • Subtype
  • Prod
  • OrderDual
  • AddOpposite
  • HasQuotient.Quotient
  • ContinuousMap
  • Additive

How is a type an instance?

Loading the hierarchy index…

Assumed by1,761

Ancestors2