mathlib3
refactor(topology/*): define and use dense_inducing
#1193

Merged

refactor(topology/*): define and use dense_inducing #1193

mergify merged 5 commits into master from extension

PatrickMassot requested a review 6 years ago

jcommelin commented on 2019-07-08

sgouezel commented on 2019-07-08

refactor(topology/*): define and dense_inducing

ed508d62

PatrickMassot commented on 2019-07-09

Apply suggestions from code review

76bd02d9

PatrickMassot commented on 2019-07-09

sgouezel commented on 2019-07-09

jcommelin changed the title ~~refactor(topology/*): define and dense_inducing~~ refactor(topology/*): define and use dense_inducing 6 years ago

jcommelin approved these changes on 2019-07-09

jcommelin added ready-to-merge

minor fixes following review

9f62a86b

mergify merged 3a7c661a into master 6 years ago

mergify deleted the extension branch 6 years ago

Some more dot notation, consistent naming and field naming

7a53c8fa

Merge branch 'master' into extension

cf153d66

Reviewers

jcommelin

sgouezel

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone