Structures · Topology
IsTopologicalGroup
A topological group is a group in which the multiplication and inversion 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 IsUniformGroup using
IsTopologicalGroup.rightUniformSpace and isUniformGroup_of_commGroup.
- Defined in
- Mathlib.Topology.Algebra.Group.Defs
- Shape
- One type argument
Extends2
Extended by3
Concrete types that are instances20
- TopCat.carrier
- SeparationQuotient
- Units
- RestrictedProduct
- Matrix.SpecialLinearGroup
- AlgEquiv
- PontryaginDual
- Circle
- ContinuousMonoidHom
- CategoryTheory.Aut
- Field.absoluteGaloisGroup
- Subtype
- Prod
- OrderDual
- Set.Elem
- ULift
- MulOpposite
- HasQuotient.Quotient
- ContinuousMap
- Multiplicative
How is a type an instance?
Loading the hierarchy index…
Assumed by586
- MeasureTheory.Measure.haarScalarFactor
- ContRepresentation.coind₁
- TopRep.resolutionX
- IsTopologicalGroup.rightUniformSpace
- TopRep.homogeneousCochains
- MeasureTheory.Measure.haar.chaar
- Subgroup.topologicalClosure
- MeasureTheory.mulEquivHaarChar
- MeasureTheory.Measure.haar
- MeasureTheory.Measure.haarMeasure
- TopRep.d
- ContRepresentation.coind₁ι
- Homeomorph.divLeft
- Homeomorph.divRight
- ContinuousCohomology.cochainsMap
- ContRepresentation.coind₁ResMap
- ContRepresentation.coind₁Map
- continuous_zpow
- MeasureTheory.Measure.haar.haarContent
- ProfiniteGrp.of
- TopRep.resolution'
- ContinuousCohomology.resolutionMap
- TopologicalGroup.IsSES.pushforward
- Multipliable.tendsto_cofinite_one
- MeasureTheory.Measure.haar.chaar_mem_clPrehaar
- TopologicalGroup.IsSES.pullback
- IsTopologicalGroup.leftUniformSpace
- ContinuousCohomology.cocyclesMap
- MeasureTheory.Measure.haar.index_pos
- ProfiniteGrp.exist_openNormalSubgroup_sub_open_nhds_of_one
- TopRep.resolution'X
- TopologicalGroup.IsSES.integrate
- ProfiniteGrp.ofHom
- continuousCohomology
- ContinuousCohomology.cocycles
- multipliable_nat_add_iff
- MeasureTheory.Measure.modularCharacterFun
- MeasureTheory.Measure.haarScalarFactor.congr_simp
- MeasureTheory.Measure.haar.index_elim
- MeasureTheory.Measure.haarScalarFactor_pos_of_isHaarMeasure
- continuous_of_continuousAt_one
- ContinuousCohomology.map
- nhds_translation_mul_inv
- map_mul_left_nhds_one
- MeasureTheory.Measure.haarMeasure_unique
- MeasureTheory.Measure.integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport
- MeasureTheory.Measure.measure_isMulInvariant_eq_smul_of_isCompact_closure
- compact_covered_by_mul_left_translates
- MeasureTheory.Measure.haarMeasure_self
- MeasureTheory.Measure.haarScalarFactor_eq_integral_div_of_continuous_nonneg_pos