σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : DecidableEq σ
m n : σ →₀ ℕ
a : R
⊢ ↑(LinearMap.stdBasis R (fun x => R) n) a m = if m = n then a else 0
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : DecidableEq σ
m n : σ →₀ ℕ
a : R
⊢ ↑(coeff R m) (↑(monomial R n) a) = if m = n then a else 0
rw [coeff, monomial_def, LinearMap.proj_apply]
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : DecidableEq σ
m n : σ →₀ ℕ
a : R
⊢ ↑(LinearMap.stdBasis R (fun x => R) n) a m = if m = n then a else 0
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : DecidableEq σ
m n : σ →₀ ℕ
a : R
⊢ ↑(LinearMap.stdBasis R (fun x => R) n) a m = if m = n then a else 0
dsimp only
no goals
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : DecidableEq σ
m n : σ →₀ ℕ
a : R
⊢ ↑(LinearMap.stdBasis R (fun x => R) n) a m = if m = n then a else 0
rw [LinearMap.stdBasis_apply, Function.update_apply, Pi.zero_apply]