mathlib3
chore(algebra/field): move some lemmas from `field` to `division_ring`
#2331

Merged

chore(algebra/field): move some lemmas from `field` to `division_ring` #2331

mergify merged 2 commits into master from div-ring

chore(algebra/field): move some lemmas from `field` to `division_ring`

05f891a4

urkud added awaiting-review

sgouezel approved these changes on 2020-04-06

sgouezel removed awaiting-review

sgouezel added ready-to-merge

Merge branch 'master' into div-ring

8c18af8b

mergify merged 3d60e134 into master 5 years ago

mergify deleted the div-ring branch 5 years ago

Reviewers

sgouezel

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone