∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₁ : Type u_2} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R₁ M₁] (n : ℕ) (x : M₁ →L[R₁] M₁), npowRecAuto (n + 1) x = npowRecAuto n x * x