σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
h : m ≠ n
a : R
⊢ ↑(coeff R m) (↑(LinearMap.stdBasis R (fun x => R) n) a) = 0
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
h : m ≠ n
a : R
⊢ ↑(coeff R m) (↑(monomial R n) a) = 0
rw [monomial_def]
no goals
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
h : m ≠ n
a : R
⊢ ↑(coeff R m) (↑(LinearMap.stdBasis R (fun x => R) n) a) = 0
exact LinearMap.stdBasis_ne R (fun _ ↦ R) _ _ h a