theorem MonomialOrder.isRemainder_range_fin {σ : Type u_2} {R : Type u_3} [CommSemiring R] {m : MonomialOrder σ} (p : MvPolynomial σ R) {ι : Type u_1} [Fintype ι] (b : ι → MvPolynomial σ R) (r : MvPolynomial σ R) : m.IsRemainder p (Set.range b) r ↔ (∃ (g : ι → MvPolynomial σ R), p = ∑ i : ι, b i * g i + r ∧ ∀ (i : ι), m.toWithBotSyn (m.withBotDegree (b i * g i)) ≤ m.toWithBotSyn (m.withBotDegree p)) ∧ ∀ c ∈ r.support, ∀ (i : ι), b i ≠ 0 → ¬m.degree (b i) ≤ c