The differential preserves multimodularity at an element

Let $M$ be a unital C*-algebra, $f$ a bounded $(n+1)$-linear map $M^{n+1}\to M$ and $r\in M$. Say $f$ is multimodular at $r$ (MultimodularAt f r) if $f(rx_0,x_1,\dots)=rf(x)$, $f(\dots,x_nr)=f(x)r$ and $f(\dots,x_jr,x_{j+1},\dots)=f(\dots,x_j,rx_{j+1},\dots)$ for all $j$. If $f$ is multimodular at $r$, then so is its Hochschild differential differential f.

Formalization Note The statement is verbatim from OpenAI's Lean development, with the listed Definitions imported in place of the upstream modules; the definitions are supporting code for this statement. Only the keyword lemma, where used upstream, becomes theorem, and a leading include ... in or omit ... in moves to the preamble. It is a step of the Lean proof of the vanishing of higher bounded Hochschild cohomology.