Commit 2023-12-12 07:30 1c9929f3

feat : direct limit and tensor product commutes (#8473) Given a family of $R$-module $G_i$'s and compatible $f : G_i \to G_j$ whenever $i \le j$ and $M$ another $R$-module, we have $\lim G_i \otimes M \cong \lim (G_i \otimes M)$