mathlib3
fix(ring_theory/adjoin_root): move adjoin_root out of adjoin_root nam…
#960

Merged

fix(ring_theory/adjoin_root): move adjoin_root out of adjoin_root nam… #960

mergify merged 1 commit into master from ChrisHughes24-patch-1

fix(ring_theory/adjoin_root): move adjoin_root out of adjoin_root nam…

826b973e

ChrisHughes24 requested a review 6 years ago

jcommelin approved these changes on 2019-04-23

jcommelin added ready-to-merge

mergify merged 0d7b4195 into master 6 years ago

mergify deleted the ChrisHughes24-patch-1 branch 6 years ago

Reviewers

jcommelin

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone