R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : R
a : A
⊢ ¬¬r ∈ σ a ↔ ¬IsUnit (↑↑ₐ r - a)
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : R
a : A
⊢ ¬r ∈ σ a ↔ IsUnit (↑↑ₐ r - a)
apply not_iff_not.mp
no goals
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : R
a : A
⊢ ¬¬r ∈ σ a ↔ ¬IsUnit (↑↑ₐ r - a)
simp [Set.not_not_mem, mem_iff]