feat(RingTheory.MvPowerSeries.Topology): define the product topology on mv power series

Mathlib.lean

@@ -3791,6 +3791,7 @@ import Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
 import Mathlib.RingTheory.MvPowerSeries.Basic
 import Mathlib.RingTheory.MvPowerSeries.Inverse
 import Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
+import Mathlib.RingTheory.MvPowerSeries.Topology
 import Mathlib.RingTheory.MvPowerSeries.Trunc
 import Mathlib.RingTheory.Nakayama
 import Mathlib.RingTheory.Nilpotent.Basic

Mathlib/RingTheory/MvPowerSeries/Basic.lean

@@ -6,6 +6,8 @@ Authors: Johan Commelin, Kenny Lau
 
 import Mathlib.Algebra.MvPolynomial.Basic
 import Mathlib.Algebra.Order.Antidiag.Finsupp
+import Mathlib.Data.Finsupp.Antidiagonal
+import Mathlib.Data.Finsupp.Weight
 import Mathlib.LinearAlgebra.StdBasis
 import Mathlib.Tactic.Linarith
 
@@ -19,6 +21,34 @@ A formal power series is to a polynomial like an infinite sum is to a finite sum
 
 We provide the natural inclusion from multivariate polynomials to multivariate formal power series.
 
+## Main definitions
+
+- `MvPowerSeries.C`: constant power series
+
+- `MvPowerSeries.X`: the indeterminates
+
+- `MvPowerSeries.coeff`, `MvPowerSeries.constantCoeff`:
+the coefficients of a `MvPowerSeries`, its constant coefficient
+
+- `MvPowerSeries.monomial`: the monomials
+
+- `MvPowerSeries.coeff_mul`: computes the coefficients of the product of two `MvPowerSeries`
+
+- `MvPowerSeries.coeff_prod` : computes the coefficients of products of `MvPowerSeries`
+
+- `MvPowerSeries.coeff_pow` : computes the coefficients of powers of a `MvPowerSeries`
+
+- `MvPowerSeries.coeff_eq_zero_of_constantCoeff_nilpotent`: if the constant coefficient
+of a `MvPowerSeries` is nilpotent, then some coefficients of its powers are automatically zero
+
+- `MvPowerSeries.map`: apply a `RingHom` to the coefficients of a `MvPowerSeries` (as a `RingHom)
+
+- `MvPowerSeries.X_pow_dvd_iff`, `MvPowerSeries.X_dvd_iff`: equivalent
+conditions for (a power of) an indeterminate to divide a `MvPowerSeries`
+
+- `MvPolynomial.toMvPowerSeries`: the canonical coercion from `MvPolynomial` to `MvPowerSeries`
+
+
 ## Note
 
 This file sets up the (semi)ring structure on multivariate power series:
@@ -621,6 +651,54 @@ theorem coeff_prod [DecidableEq σ]
       simp only [add_right_inj] at huv
       exact h rfl huv.symm
 
+/-- The `d`th coefficient of a power of a multivariate power series
+is the sum, indexed by `finsuppAntidiag (Finset.range n) d`, of products of coefficients  -/
+theorem coeff_pow [DecidableEq σ] (f : MvPowerSeries σ R) {n : ℕ} (d : σ →₀ ℕ) :
+    coeff R d (f ^ n) =
+      ∑ l in finsuppAntidiag (Finset.range n) d,
+        ∏ i in Finset.range n, coeff R (l i) f := by
+  suffices f ^ n = (Finset.range n).prod fun _ ↦ f by
+    rw [this, coeff_prod]
+  rw [Finset.prod_const, card_range]
+
+/-- Vanishing of coefficients of powers of multivariate power series
+when the constant coefficient is nilpotent
+[N. Bourbaki, *Algebra {II}*, Chapter 4, §4, n°2, proposition 3][bourbaki1981] -/
+theorem coeff_eq_zero_of_constantCoeff_nilpotent [DecidableEq σ]
+    {f : MvPowerSeries σ R} {m : ℕ} (hf : constantCoeff σ R f ^ m = 0)
+    {d : σ →₀ ℕ} {n : ℕ} (hn : m + degree d ≤ n) : coeff R d (f ^ n) = 0 := by
+  rw [coeff_pow]
+  apply sum_eq_zero
+  intro k hk
+  rw [mem_finsuppAntidiag] at hk
+  set s := (range n).filter fun i ↦ k i = 0 with hs_def
+  have hs : s ⊆ range n := filter_subset _ _
+  have hs' (i : ℕ) (hi : i ∈ s) : coeff R (k i) f = constantCoeff σ R f := by
+    simp only [hs_def, mem_filter] at hi
+    rw [hi.2, coeff_zero_eq_constantCoeff]
+  have hs'' (i : ℕ) (hi : i ∈ s) : k i = 0 := by
+    simp only [hs_def, mem_filter] at hi
+    rw [hi.2]
+  rw [← prod_sdiff (s₁ := s) (filter_subset _ _)]
+  apply mul_eq_zero_of_right
+  rw [prod_congr rfl hs', prod_const]
+  suffices m ≤ s.card by
+    obtain ⟨m', hm'⟩ := Nat.exists_eq_add_of_le this
+    rw [hm', pow_add, hf, MulZeroClass.zero_mul]
+  rw [← Nat.add_le_add_iff_right, add_comm s.card,
+    Finset.card_sdiff_add_card_eq_card (filter_subset _ _), card_range]
+  apply le_trans _ hn
+  simp only [add_comm m, Nat.add_le_add_iff_right, ← hk.1,
+    ← sum_sdiff (hs), sum_eq_zero (s := s) hs'', add_zero]
+  rw [← hs_def]
+  convert Finset.card_nsmul_le_sum (range n \ s) (fun x ↦ degree (k x)) 1 _
+  · simp only [Algebra.id.smul_eq_mul, mul_one]
+  · simp only [degree_eq_weight_one, map_sum]
+  · simp only [hs_def, mem_filter, mem_sdiff, mem_range, not_and, and_imp]
+    intro i hi hi'
+    rw [← not_lt, Nat.lt_one_iff, degree_eq_zero_iff]
+    exact hi' hi
+
 end CommSemiring
 
 section Algebra