AddGroupFilterBasis.uniformAddGroup

theorem AddGroupFilterBasis.uniformAddGroup : ∀ {G : Type u_1} [inst : AddCommGroup G] (B : AddGroupFilterBasis G), UniformAddGroup G

This theorem states that for any given type `G` which is an additive commutative group, and any additive group filter basis `B` on `G`, the uniform space structure that is derived from `B` via the corresponding topological abelian group structure is compatible with its group structure. In other words, the topology of `G` induced by the filter basis `B` obeys the axioms of a uniform add group.

More concisely: For any additive commutative group `(G, +)` and its additive group filter basis `B`, the uniform space structure derived from `B` turns `(G, +)` into a uniform add group.