R S : Type u
x y : R
inst✝² : MonoidWithZero R
inst✝¹ : MonoidWithZero S
r : R
F : Type u_1
inst✝ : MonoidWithZeroHomClass F R S
hr : IsNilpotent r
f : F
⊢ ↑f r ^ Exists.choose hr = 0
R S : Type u
x y : R
inst✝² : MonoidWithZero R
inst✝¹ : MonoidWithZero S
r : R
F : Type u_1
inst✝ : MonoidWithZeroHomClass F R S
hr : IsNilpotent r
f : F
⊢ IsNilpotent (↑f r)
use hr.choose
no goals
R S : Type u
x y : R
inst✝² : MonoidWithZero R
inst✝¹ : MonoidWithZero S
r : R
F : Type u_1
inst✝ : MonoidWithZeroHomClass F R S
hr : IsNilpotent r
f : F
⊢ ↑f r ^ Exists.choose hr = 0
rw [← map_pow, hr.choose_spec, map_zero]