mathlib

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

feat(ring_theory/polynomial): refactor of is_integral_domain_fin (#2119) * chore(ring_theory/polynomial): refactor proof of is_noetherian_ring_fin * not there yet * feat(ring_theory/polynomial): refactor of is_integral_domain_fin * fix * refactor * fix * fix * suggestion from linter * Update src/data/mv_polynomial.lean Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>