σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : DecidableEq σ
n : σ →₀ ℕ
⊢ LinearMap.stdBasis R (fun x => R) n = LinearMap.stdBasis R (fun x => R) n
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : DecidableEq σ
n : σ →₀ ℕ
⊢ monomial R n = LinearMap.stdBasis R (fun x => R) n
rw [monomial]
no goals
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : DecidableEq σ
n : σ →₀ ℕ
⊢ LinearMap.stdBasis R (fun x => R) n = LinearMap.stdBasis R (fun x => R) n
convert rfl