mathlib3
feat(topology/constructions): distributivity of products over sums
#1059

Merged

feat(topology/constructions): distributivity of products over sums #1059

mergify merged 6 commits into master from rwbarton-distrib

feat(topology/constructions): distributivity of products over sums

3dbdc5f9

rwbarton requested a review 6 years ago

jcommelin commented on 2019-05-20

sgouezel commented on 2019-07-01

jcommelin requested changes on 2019-07-08

cipher1024 assigned

jcommelin 6 years ago

Update src/topology/maps.lean

02f6850a

Merge remote-tracking branch 'origin/master' into HEAD

9fda5170

Reverse direction of sigma_prod_distrib

7edef0ed

jcommelin approved these changes on 2019-09-07

jcommelin added ready-to-merge

Merge branch 'master' into rwbarton-distrib

779f79da

Merge branch 'master' into rwbarton-distrib

cc618e8d

mergify merged 10cb0d12 into master 6 years ago

mergify deleted the rwbarton-distrib branch 6 years ago

Reviewers

jcommelin

sgouezel

ChrisHughes24

Assignees

jcommelin

Labels

ready-to-merge

Milestone

No milestone