Commit 2025-05-21 12:33 4e7f8d4a

chore(RingTheory/MvPowerSeries/PiTopology): limit of truncation of power series (#23643) Extract a lemma that says that for a multivariate power series, trunc' R d f converges to f when d converges to infinity. Prove the analogous lemma for MvPowerSeries.trunc (if the set of indeterminates is nonempty). Move this lemma and the denseness of polynomials to the PiTopology file.