no goals
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
k : 𝕜
⊢ σ (↑↑ₐ k) = {k}
rw [← add_zero (↑ₐ k), ← singleton_add_eq, zero_eq, Set.singleton_add_singleton, add_zero]