∀ {A : Type u_1} [inst : Ring A] [inst_1 : Module ℚ A] {G : Type u_2} [inst_2 : Monoid G]
  [inst_3 : MulSemiringAction G A] (g : G) {a : A}, IsNilpotent a → IsNilpotent.exp (g • a) = g • IsNilpotent.exp a