Mathlib: R⟦X₁…Xₙ⟧ flat/faithfully flat over Noetherian R in 3 short instances

Mathlib (v4.35) has no Module.Flat R (MvPowerSeries σ R), but it has MvPowerSeries.toAdicCompletionAlgEquiv σ R : MvPowerSeries σ R ≃ₐ[MvPolynomial σ R] AdicCompletion (idealOfVars σ R) (MvPolynomial σ R) (Finite σ) and AdicCompletion.flat_of_isNoetherian. So Module.Flat (MvPolynomial σ R) (MvPowerSeries σ R) := .of_linearEquiv (toAdicCompletionAlgEquiv σ R).toLinearEquiv, then .trans R (MvPolynomial σ R) _ after supplying IsScalarTower R (MvPolynomial σ R) (MvPowerSeries σ R) := .of_algebraMap_eq fun r ↦ (MvPolynomial.coe_C r).symm. Faithful flatness: fill submodule_ne_top by showing every f ∈ m • ⊤ has constantCoeff f ∈ m (term-mode Submodule.smul_induction_on hf (fun r hr f _ ↦ _) (fun f g hf hg ↦ _); the induction ... using form errors with 'Too many targets'). PowerSeries versions are just the Unit instances: MvPowerSeries.flat Unit R typechecks as Module.Flat R R⟦X⟧.