R S : Type u
x y : R
inst✝ : Ring R
h_comm✝ : Commute x y
h_comm : Commute x (-y)
hx : IsNilpotent x
hy : IsNilpotent y
⊢ IsNilpotent (x - y)
R S : Type u
x y : R
inst✝ : Ring R
h_comm : Commute x y
hx : IsNilpotent x
hy : IsNilpotent y
⊢ IsNilpotent (x - y)
rw [← neg_right_iff] at h_comm
R S : Type u
x y : R
inst✝ : Ring R
h_comm✝ : Commute x y
h_comm : Commute x (-y)
hx : IsNilpotent x
hy : IsNilpotent (-y)
⊢ IsNilpotent (x - y)
R S : Type u
x y : R
inst✝ : Ring R
h_comm✝ : Commute x y
h_comm : Commute x (-y)
hx : IsNilpotent x
hy : IsNilpotent y
⊢ IsNilpotent (x - y)
rw [← isNilpotent_neg_iff] at hy
R S : Type u
x y : R
inst✝ : Ring R
h_comm✝ : Commute x y
h_comm : Commute x (-y)
hx : IsNilpotent x
hy : IsNilpotent (-y)
⊢ IsNilpotent (x + -y)
R S : Type u
x y : R
inst✝ : Ring R
h_comm✝ : Commute x y
h_comm : Commute x (-y)
hx : IsNilpotent x
hy : IsNilpotent (-y)
⊢ IsNilpotent (x - y)
rw [sub_eq_add_neg]
no goals
R S : Type u
x y : R
inst✝ : Ring R
h_comm✝ : Commute x y
h_comm : Commute x (-y)
hx : IsNilpotent x
hy : IsNilpotent (-y)
⊢ IsNilpotent (x + -y)
exact h_comm.isNilpotent_add hx hy