continuous_functions): the ring of continuous functions
#923

Merged

feat(topology/algebra/continuous_functions): the ring of continuous functions #923

mergify merged 4 commits into master from ring-continuous-functions

feat(topology/algebra/continuous_functions): the ring of continuous f…

531a03d0

kim-em requested a review 7 years ago

jcommelin commented on 2019-04-11

filling in the hierarchy

c5b217a2

cipher1024 assigned

jcommelin 7 years ago

jcommelin commented on 2019-04-15

use to_additive

274f7807

Merge branch 'master' into ring-continuous-functions

8e13e190

jcommelin added ready-to-merge

jcommelin approved these changes on 2019-04-15

mergify merged d06eb858 into master 7 years ago

mergify deleted the ring-continuous-functions branch 7 years ago

Reviewers

jcommelin

Assignees

jcommelin

Labels

ready-to-merge

Milestone

No milestone