case intro
R S : Type u
x y : R
inst✝ : Semiring R
h_comm : Commute x y
n : ℕ
hn : x ^ n = 0
⊢ IsNilpotent (x * y)
R S : Type u
x y : R
inst✝ : Semiring R
h_comm : Commute x y
h : IsNilpotent x
⊢ IsNilpotent (x * y)
obtain ⟨n, hn⟩ := h
case intro
R S : Type u
x y : R
inst✝ : Semiring R
h_comm : Commute x y
n : ℕ
hn : x ^ n = 0
⊢ (x * y) ^ n = 0
case intro
R S : Type u
x y : R
inst✝ : Semiring R
h_comm : Commute x y
n : ℕ
hn : x ^ n = 0
⊢ IsNilpotent (x * y)
use n
no goals
case intro
R S : Type u
x y : R
inst✝ : Semiring R
h_comm : Commute x y
n : ℕ
hn : x ^ n = 0
⊢ (x * y) ^ n = 0
rw [h_comm.mul_pow, hn, MulZeroClass.zero_mul]