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