Uniform structure on topological groups
extension of ℤ-bilinear maps to complete groups (useful for ring completions)
A uniform (additive) group is a group in which the addition and negation are uniformly continuous.
The right uniformity on a topological group.
- add_left : ∀ (a a' : α) (b : β), f (a + a', b) = f (a, b) + f (a', b)
- add_right : ∀ (a : α) (b b' : β), f (a, b + b') = f (a, b) + f (a, b')
ℤ-bilinearity for maps between additive commutative groups.
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.