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
h : Decidable (a = 0)
⊢ support (↑(monomial s) a) = if a = 0 then ∅ else {s}
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
h : Decidable (a = 0)
⊢ support (↑(monomial s) a) = if a = 0 then ∅ else {s}
rw [←Subsingleton.elim (Classical.decEq R a 0) h]
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
h : Decidable (a = 0)
⊢ support (↑(monomial s) a) = if a = 0 then ∅ else {s}
rfl