mathlib

f0bb2f82 - feat(ring_theory/polynomial): mv_polynomial.integral_domain (#2021)

feat(ring_theory/polynomial): mv_polynomial.integral_domain (#2021) * feat(ring_theory/polynomial): mv_polynomial.integral_domain * Add docstrings * Add docstrings * Fix import * Fix build * Please linter, please * Update src/algebra/ring.lean * Clean up code, process comments * Update src/data/equiv/fin.lean * Update src/data/equiv/fin.lean * Update src/data/equiv/fin.lean * Update src/ring_theory/polynomial.lean Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Scott Morrison <scott@tqft.net> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>