feat(ring_theory/power_series): several simp lemmas (#1945)

* Small start on generating functions

* Playing with Bernoulli

* Finished sum_bernoulli

* Some updates after PRs

* Analogue for mv_power_series

* Cleanup after merged PRs

* feat(ring_theory/power_series): several simp lemmas

* Remove file that shouldn't be there yet

* Update src/ring_theory/power_series.lean

Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr>

* Generalise lemma to canonically_ordered_monoid

* Update name

* Fix build

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

Author: 3 people

src/data/finsupp.lean

@@ -384,6 +384,7 @@ instance nat_sub : has_sub (α →₀ ℕ) := ⟨zip_with (λ m n, m - n) (nat.s
 
 @[simp] lemma nat_sub_apply {g₁ g₂ : α →₀ ℕ} {a : α} :
   (g₁ - g₂) a = g₁ a - g₂ a := rfl
+
 end nat_sub
 
 section add_monoid
@@ -1488,6 +1489,21 @@ lemma le_iff [canonically_ordered_monoid α] (f g : σ →₀ α) :
 ⟨λ h s hs, h s,
 λ h s, if H : s ∈ f.support then h s H else (not_mem_support_iff.1 H).symm ▸ zero_le (g s)⟩
 
+@[simp] lemma add_eq_zero_iff [canonically_ordered_monoid α] (f g : σ →₀ α) :
+  f + g = 0 ↔ f = 0 ∧ g = 0 :=
+begin
+  split,
+  { assume h,
+    split,
+    all_goals
+    { ext s,
+      suffices H : f s + g s = 0,
+      { rw add_eq_zero_iff at H, cases H, assumption },
+      show (f + g) s = 0,
+      rw h, refl } },
+  { rintro ⟨rfl, rfl⟩, simp }
+end
+
 attribute [simp] to_multiset_zero to_multiset_add
 
 @[simp] lemma to_multiset_to_finsupp (f : σ →₀ ℕ) :

src/data/mv_polynomial.lean

@@ -346,7 +346,7 @@ begin
     delta X monomial at hi', rw mem_support_single at hi', cases hi', subst i',
     erw finset.mem_singleton at H, subst m,
     rw [mem_support_iff, add_apply, single_apply, if_pos rfl],
-    intro H, rw [add_eq_zero_iff] at H, exact one_ne_zero H.2 }
+    intro H, rw [_root_.add_eq_zero_iff] at H, exact one_ne_zero H.2 }
 end
 
 end coeff

src/data/polynomial.lean

@@ -2006,7 +2006,7 @@ have hq0 : q ≠ 0, from λ hp0, by simpa [hp0] using hq,
 have nat_degree (1 : polynomial α) = nat_degree (p * q),
   from congr_arg _ hq,
 by rw [nat_degree_one, nat_degree_mul_eq hp0 hq0, eq_comm,
-    add_eq_zero_iff, ← with_bot.coe_eq_coe,
+    _root_.add_eq_zero_iff, ← with_bot.coe_eq_coe,
     ← degree_eq_nat_degree hp0] at this;
   exact this.1
 

src/ring_theory/power_series.lean

@@ -316,6 +316,32 @@ lemma coeff_X_pow (m : σ →₀ ℕ) (s : σ) (n : ℕ) :
   coeff α m ((X s : mv_power_series σ α)^n) = if m = single s n then 1 else 0 :=
 by rw [X_pow_eq s n, coeff_monomial]
 
+@[simp] lemma coeff_mul_C (n : σ →₀ ℕ) (φ : mv_power_series σ α) (a : α) :
+  coeff α n (φ * (C σ α a)) = (coeff α n φ) * a :=
+begin
+  rw [coeff_mul n φ], rw [finset.sum_eq_single (n,(0 : σ →₀ ℕ))],
+  { rw [coeff_C, if_pos rfl] },
+  { rintro ⟨i,j⟩ hij hne,
+    rw finsupp.mem_antidiagonal_support at hij,
+    by_cases hj : j = 0,
+    { subst hj, simp at *, contradiction },
+    { rw [coeff_C, if_neg hj, mul_zero] } },
+  { intro h, exfalso, apply h,
+    rw finsupp.mem_antidiagonal_support,
+    apply add_zero }
+end
+
+@[simp] lemma coeff_zero_mul_X (φ : mv_power_series σ α) (s : σ) :
+  coeff α (0 : σ →₀ ℕ) (φ * X s) = 0 :=
+begin
+  rw [coeff_mul _ φ, finset.sum_eq_zero],
+  rintro ⟨i,j⟩ hij,
+  obtain ⟨rfl, rfl⟩ : i = 0 ∧ j = 0,
+  { rw finsupp.mem_antidiagonal_support at hij,
+    simpa using hij },
+  simp,
+end
+
 variables (σ) (α)
 
 /-- The constant coefficient of a formal power series.-/
@@ -896,6 +922,31 @@ begin
       exact ⟨finsupp.unique_single f, finsupp.unique_single g⟩ } }
 end
 
+@[simp] lemma coeff_mul_C (n : ℕ) (φ : power_series α) (a : α) :
+  coeff α n (φ * (C α a)) = (coeff α n φ) * a :=
+mv_power_series.coeff_mul_C _ φ a
+
+@[simp] lemma coeff_succ_mul_X (n : ℕ) (φ : power_series α) :
+  coeff α (n+1) (φ * X) = coeff α n φ :=
+begin
+  rw [coeff_mul _ φ, finset.sum_eq_single (n,1)],
+  { rw [coeff_X, if_pos rfl, mul_one] },
+  { rintro ⟨i,j⟩ hij hne,
+    by_cases hj : j = 1,
+    { subst hj, simp at *, contradiction },
+    { simp [coeff_X, hj] } },
+  { intro h, exfalso, apply h, simp },
+end
+
+@[simp] lemma coeff_zero_mul_X (φ : power_series α) :
+  coeff α 0 (φ * X) = 0 :=
+begin
+  rw [coeff_mul _ φ, finset.sum_eq_zero],
+  rintro ⟨i,j⟩ hij,
+  obtain ⟨rfl, rfl⟩ : i = 0 ∧ j = 0, { simpa using hij },
+  simp,
+end
+
 @[simp] lemma constant_coeff_C (a : α) : constant_coeff α (C α a) = a := rfl
 @[simp] lemma constant_coeff_comp_C :
   (constant_coeff α).comp (C α) = ring_hom.id α := rfl