exact IsNilpotent.zero
case neg
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsNilpotent x
hS : ¬∃ s, Nonempty (Basis { x // x ∈ s } R S)
⊢ IsNilpotent 0
no goals