feat(RingTheory/MvPowerSeries): adic completeness for MvPowerSeries (#35846)

This PR continues the work in #35670 and #35707 by adding typeclass instances for the completeness of `MvPowerSeries` when the index type is finite.

Author: BryceT233

Mathlib/RingTheory/AdicCompletion/Completeness.lean

@@ -8,6 +8,10 @@ module
 public import Mathlib.Algebra.Lie.OfAssociative
 public import Mathlib.RingTheory.AdicCompletion.Exactness
 public import Mathlib.RingTheory.Finiteness.Ideal
+public import Mathlib.RingTheory.MvPowerSeries.Equiv
+public import Mathlib.RingTheory.PowerSeries.Basic
+
+import Mathlib.RingTheory.AdicCompletion.Topology
 
 /-!
 # Completeness of the Adic Completion for Finitely Generated Ideals
@@ -32,6 +36,9 @@ when the ideal `I` is finitely generated.
 * `AdicCompletion.isAdicComplete`: `AdicCompletion I M` is `I`-adically complete if `I` is
   finitely generated.
 
+* `MvPowerSeries.isAdicComplete`: Multivariate power series is adic complete with respect to
+  the ideal spanned by all variables when the index is finite.
+
 -/
 
 public section
@@ -188,3 +195,27 @@ theorem isAdicComplete (h : I.FG) : IsAdicComplete I (AdicCompletion I M) where
     simp [L]
 
 end AdicCompletion
+
+namespace MvPowerSeries
+
+instance {σ : Type*} [Finite σ] :
+    IsAdicComplete (.span (.range X) : Ideal (MvPowerSeries σ R)) (MvPowerSeries σ R) := by
+  have : Ideal.map (toAdicCompletionAlgEquiv σ R).toRingEquiv (Ideal.span (Set.range X)) =
+    (MvPolynomial.idealOfVars σ R).map (algebraMap ..):= by
+    simp_rw [Ideal.map_span, ← Set.range_comp]
+    congr 2; ext1
+    simp [AdicCompletion.algebraMap_apply, ← MvPolynomial.coe_X, toAdicCompletion_coe]
+  rw [← IsAdicComplete.congr_ringEquiv _ (toAdicCompletionAlgEquiv σ R).toRingEquiv, this,
+    IsAdicComplete.map_algebraMap_iff]
+  exact AdicCompletion.isAdicComplete (MvPolynomial.idealOfVars_fg σ R)
+
+end MvPowerSeries
+
+namespace PowerSeries
+
+instance : IsAdicComplete (.span {X} : Ideal (PowerSeries R)) (PowerSeries R) := by
+  have : IsAdicComplete (.span (.range MvPowerSeries.X) : Ideal (MvPowerSeries Unit R))
+    (MvPowerSeries Unit R) := inferInstance
+  rwa [Set.range_unique] at this
+
+end PowerSeries