Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-07-18 15:15 8b102eb2

View on Github →

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

Estimated changes

deleted theorem set.mul_subset_mul
added theorem filter.tendsto_mul_mul
added theorem is_closed_map_mul_left
added def nhds_is_mul_hom
added theorem nhds_pointwise_mul