mathlib3

8b102eb2 - feat(topology/algebra/group): define filter pointwise addition (#1215)

feat(topology/algebra/group): define filter pointwise addition (#1215) * Create .DS_Store * Revert "Create .DS_Store" This reverts commit 5612886d493aef59205eddc5a34a75e6e5ba22c1. * feat (topology/algebral/uniform_group) : prove dense_embedding.extend extends continuous linear maps linearly * Update src/algebra/pointwise.lean Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr> * Fix styles * Add homomorphism instances; fix conflicting names * Update group.lean * Update uniform_group.lean * Add header; prove every topological group is regular * Fix headers and errors * Update pi_instances.lean