R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
⊢ coeff m (p * ↑(monomial s) r) = if s ≤ m then coeff (m - s) p * r else 0
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
⊢ coeff m (↑(monomial s) r * p) = if s ≤ m then r * coeff (m - s) p else 0
rw [mul_comm, mul_comm r]
no goals
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
⊢ coeff m (p * ↑(monomial s) r) = if s ≤ m then coeff (m - s) p * r else 0
exact coeff_mul_monomial' _ _ _ _