mathlib3
feat(topology/algebra/group): define filter pointwise addition
#1215
Merged
Merged
feat(topology/algebra/group): define filter pointwise addition #1215
mergify
merged
21 commits into
leanprover-community:master
from
linearly_extend
Create .DS_Store
5612886d
Revert "Create .DS_Store"
e0209f74
Merge branch 'master' of https://github.com/leanprover-community/mathlib
6e5694b3
erge branch 'master' of https://github.com/leanprover-community/mathlib
ab19e053
Merge branch 'master' of https://github.com/leanprover-community/mathlib
443ea2b3
feat (topology/algebral/uniform_group) : prove dense_embedding.extend…
a9af706f
Update src/algebra/pointwise.lean
e229bf46
Fix styles
6eeeb712
Add homomorphism instances; fix conflicting names
94b69f3d
Merge branch 'linearly_extend' of https://github.com/aceg00/mathlib i…
cee3cf97
Merge branch 'master' into linearly_extend
3fa46afc
Update group.lean
1f012b97
Update uniform_group.lean
e7347f4f
aceg00
changed the title
Merge branch 'master' into linearly_extend
9d5821ad
jcommelin
commented
on 2019-07-12
Add header; prove every topological group is regular
6ea2e5eb
Merge branch 'linearly_extend' of https://github.com/aceg00/mathlib i…
c092d12a
jcommelin
commented
on 2019-07-13
Fix headers and errors
7eea3371
Merge branch 'master' into linearly_extend
e315d5b5
Merge branch 'master' into linearly_extend
31f1127f
Update pi_instances.lean
26b2bec5
avigad
approved these changes
on 2019-07-18
![mergify[bot]](https://avatars.githubusercontent.com/in/10562?v=4&s=60)
Merge branch 'master' into linearly_extend
fb1de225
Login to write a write a comment.
Login via GitHub