no goals
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
x : R
⊢ x ∈ -σ a ↔ x ∈ σ (-a)
simp only [mem_neg, mem_iff, map_neg, ← neg_add', IsUnit.neg_iff, sub_neg_eq_add]