Identity commutator cyclic ladder (source code)

= Identity commutator cyclic ladder
{title2=$AB^iy=iB^{i-1}y$}

For real-linear operators $[A,B]=I$ and a nonzero vector $y$ with $Ay=0$, induction gives $[A,B^i]=iB^{i-1}$, hence the displayed formula. Applying $A^n$ to a nontrivial finite dependence with highest term $c_nB^ny$ leaves $n!c_ny$, a contradiction. Thus $y,By,B^2y,\ldots$ are linearly independent, and their span is invariant under both operators. Characteristic zero is essential to the factorial argument.