Lemma 2.15, p. 17 — for t ∈ I with t·I⁻¹ coprime to J, u ↦ t·u induces an R-module isomorphism M/JM → IM/IJM

Let $K$ be a number field with ring of integers $R = \mathcal{O}_K$, let $I, J \subseteq R$ be nonzero ideals, let $t \in I$ be such that the ideal $t\cdot I^{-1} \subseteq R$ is coprime to $J$ (that is, $t\cdot I^{-1} + J = R$), and let $M$ be a nonzero fractional ideal of $K$. Consider the $R$-linear map

Then $\theta_t$ is surjective and its kernel is exactly $JM$. Equivalently, multiplication by $t$ induces an isomorphism of $R$-modules

The lemma lets one replace an arbitrary ideal $I$ by the ring $R$ itself modulo $q$: with $J = \langle q\rangle$ and $M = R$ it identifies $R/qR$ with $I/qI$, and with $M = I^\vee$ it identifies $I^\vee/qI^\vee$ with $R^\vee/qR^\vee$. Both reductions of the paper (§4.2 and §5) rest on these identifications.

Formalization Note The paper's sentence "Moreover, this isomorphism may be efficiently inverted given $I, J, M$, and $t$" is algorithmic and is not formalized. The hypotheses $I \neq 0$, $J \neq 0$, $M \neq 0$ express the paper's convention that ideals are nonzero (footnote 2, p. 13); $I \neq 0$ is essential because Lean sets $0^{-1} = 0$. The isomorphism is stated through the given map (surjectivity and kernel), not as the bare existence of some isomorphism, which would hold for unrelated reasons.