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
inst✝ : DecidableEq σ
i : σ
m : σ →₀ ℕ
k : ℕ
this : coeff m (↑(monomial (Finsupp.single i k)) 1) = if Finsupp.single i k = m then 1 else 0
⊢ coeff m (X i ^ k) = if Finsupp.single i k = m then 1 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
inst✝ : DecidableEq σ
i : σ
m : σ →₀ ℕ
k : ℕ
⊢ coeff m (X i ^ k) = if Finsupp.single i k = m then 1 else 0
have := coeff_monomial m (Finsupp.single i k) (1 : R)
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
inst✝ : DecidableEq σ
i : σ
m : σ →₀ ℕ
k : ℕ
this : coeff m (Finsupp.prod (Finsupp.single i k) fun n e => X n ^ e) = if Finsupp.single i k = m then 1 else 0
⊢ X i ^ 0 = 1
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
inst✝ : DecidableEq σ
i : σ
m : σ →₀ ℕ
k : ℕ
this : coeff m (↑(monomial (Finsupp.single i k)) 1) = if Finsupp.single i k = m then 1 else 0
⊢ coeff m (X i ^ k) = if Finsupp.single i k = m then 1 else 0
rwa [@monomial_eq _ _ (1 : R) (Finsupp.single i k) _, C_1, one_mul, Finsupp.prod_single_index]
  at this
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
inst✝ : DecidableEq σ
i : σ
m : σ →₀ ℕ
k : ℕ
this : coeff m (Finsupp.prod (Finsupp.single i k) fun n e => X n ^ e) = if Finsupp.single i k = m then 1 else 0
⊢ X i ^ 0 = 1
exact pow_zero _