mathlib3
feat(ring_theory/polynomial): refactor of is_integral_domain_fin
#2119

Merged

feat(ring_theory/polynomial): refactor of is_integral_domain_fin #2119

mergify merged 12 commits into master from is_integral_domain_fin

chore(ring_theory/polynomial): refactor proof of is_noetherian_ring_fin

0fae3fae

not there yet

15fe8bed

Merge branch 'is_noetherian_ring_fin_refactor' into is_integral_domai…

e0c9a490

feat(ring_theory/polynomial): refactor of is_integral_domain_fin

67cee3cd

fix

0646b4fa

refactor

43a61aee

fix

8afbcb0c

fix

1f4e2f46

merge

b2edb13d

kim-em commented on 2020-03-10

suggestion from linter

a9ee0e99

jcommelin approved these changes on 2020-03-10

Update src/data/mv_polynomial.lean

32716047

jcommelin added ready-to-merge

Merge branch 'master' into is_integral_domain_fin

aa2428a8

mergify merged 9feefee8 into master 6 years ago

mergify deleted the is_integral_domain_fin branch 6 years ago

Reviewers

jcommelin

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone