Idempotent–unit splitting for an element coprime to its annihilating factor

Let $R$ be a commutative ring and let $f, g \in R$ satisfy $f g = 0$ and, in addition, the Bézout condition that $f$ and $g$ are coprime in the Mathlib sense, i.e. there exist $u, v \in R$ with $u f + v g = 1$. The theorem asserts the existence of elements $e, w \in R$ such that $e$ is idempotent ($e \cdot e = e$), $w$ is a unit of $R$, and $f = e w$. Thus any element of a commutative ring which annihilates an element coprime to it factors as an idempotent times a unit; equivalently, $f$ generates the same ideal as an idempotent. The statement is existential only: no canonicity or uniqueness of $e$ and $w$ is claimed, although the witnesses produced in the proof are $e = u f$ and $w = f + (1 - u f)$ for any chosen Bézout pair $(u,v)$.

This is the algebraic form of the fact that the vanishing locus of $f$ is open and closed in $\operatorname{Spec} R$ when $f$ has a coprime annihilator, so that $(f)$ is generated by an idempotent; in particular such an $f$ that is nilpotent must vanish. It is used in the verification of the $\Gamma_1$-link criterion ModularCurve.IsGamma1Link.of_map_of_surjective_of_ker_pow_eq_bot, where divisibility by a separable kernel polynomial is lifted along a nilpotent thickening.