Discrete topological groups have the discrete uniformity

A complement to Mathlib's DiscreteUniformity: a right-uniform additive group whose topology is discrete has the discrete uniformity, since its uniformity is the comap of the (discrete) neighbourhood filter of zero.

Main results

• DiscreteUniformity.of_discreteTopology : a right-uniform additive group with discrete topology has the discrete uniformity. Stated as a theorem, not an instance: together with Mathlib's DiscreteUniformity → DiscreteTopology instance it would form a resolution cycle. It lives in the root DiscreteUniformity namespace it extends, following this repository's convention for lemmas about external types.

theorem DiscreteUniformity.of_discreteTopology {G : Type u_1} [AddGroup G] [UniformSpace G] [IsRightUniformAddGroup G] [DiscreteTopology G] : DiscreteUniformity G

A right-uniform additive group whose topology is discrete has the discrete uniformity.

A theorem rather than an instance: Mathlib's DiscreteUniformity → DiscreteTopology instance points the other way, and registering both directions would loop.