R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r x : R
⊢ (fun x x_1 => x + x_1) (-r) x ∈ σ a ↔ x ∈ σ (↑↑ₐ r + a)
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r x : R
⊢ x ∈ {r} + σ a ↔ x ∈ σ (↑↑ₐ r + a)
rw [singleton_add, image_add_left, mem_preimage]
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r x : R
⊢ -r + x ∈ σ a ↔ x ∈ σ (↑↑ₐ r + a)
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r x : R
⊢ (fun x x_1 => x + x_1) (-r) x ∈ σ a ↔ x ∈ σ (↑↑ₐ r + a)
simp only
no goals
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r x : R
⊢ -r + x ∈ σ a ↔ x ∈ σ (↑↑ₐ r + a)
rw [add_comm, add_mem_iff, map_neg, neg_neg]