multiplication on MvPolynomial should be irreducible

Stream: mathlib4

[Floris van Doorn]

Can we make multiplication on MvPolynomial irreducible? The following example takes 30+ seconds to time-out, because Lean starts unfolding everything.

import Mathlib.RingTheory.Polynomial.Basic

set_option maxHeartbeats 10000000
set_option profiler true
set_option trace.profiler true
example [CommRing R] [IsDomain R] (a b c : MvPolynomial ι R) (ha : a ≠ 0) :
  a * b = a * c ↔ b = c := mul_left_inj' ha -- error. `mul_right_inj' ha` is the correct proof

[Floris van Doorn]

(this also causes by exact? to be very slow)

[Eric Wieser]

I think we should do this for MonoidAlgebra instead

[Floris van Doorn]

This example fails ~1200x faster on #12554.