∀ {R : Type u_1} {σ : Type u_2} [inst : CommRing R] [NoZeroDivisors R] {p : MvPolynomial σ R} {n : σ →₀ ℕ},
  p ∣ (MvPolynomial.monomial n) 1 ↔ ∃ m u, m ≤ n ∧ IsUnit u ∧ p = (MvPolynomial.monomial m) u