mathlib3

61b0f419 - refactor(data/{mv_,}polynomial): lemmas about `adjoin` (#10670)

refactor(data/{mv_,}polynomial): lemmas about `adjoin` (#10670) Prove `adjoin {X} = ⊤` and `adjoin (range X) = ⊤` for `polynomial`s and `mv_polynomial`s much earlier and use these equalities to golf some proofs. Also drop some `comm_` in typeclass assumptions.