Nilpotence under zero-preserving multiplicative maps

A positive vanishing exponent transports through a multiplicative map even when that map does not preserve the identity.

theorem RS.isNilpotent_map_of_mul_zero {A : Type u_1} {B : Type u_2} [MonoidWithZero A] [MonoidWithZero B] (F : A → B) (hzero : F 0 = 0) (hmul : ∀ (a b : A), F (a * b) = F a * F b) {x : A} (hx : IsNilpotent x) : IsNilpotent (F x)

A zero-preserving multiplicative map preserves nilpotence.