mathlib3

62acd6b8 - chore(CommRing/adjunctions): refactor proofs (#1049)

chore(CommRing/adjunctions): refactor proofs (#1049) * splitting adjunction.lean * chore(CommRing/adjunctions): refactor proofs * remove unnecessary assumptions * add helpful doc-string * cleanup * breaking things, haven't finished yet * deterministic timeout * unfold_coes to the rescue * one more int.cast * yet another int.cast * Update src/data/mv_polynomial.lean Co-Authored-By: Johan Commelin <johan@commelin.net> * Update src/data/mv_polynomial.lean Co-Authored-By: Johan Commelin <johan@commelin.net> * WIP * Fix build * Fix build