uniform_add_group

A uniform (additive) group is a group in which the addition and negation are uniformly continuous.

dense_inducing.extend_Z_bilin

Bourbaki GT III.6.5 Theorem I: ℤ-bilinear continuous maps from dense images into a complete Hausdorff group extend by continuity. Note: Bourbaki assumes that α and β are also complete Hausdorff, but this is not necessary.