feat(ring_theory/laurent): coe from R[[x]] to R((x)) (#11318)

And actually the changes reported in #11295
Generalize `power_series.coeff_smul`



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

src/ring_theory/hahn_series.lean

@@ -997,6 +997,47 @@ lemma of_power_series_apply_coeff (x : power_series R) (n : ℕ) :
   (of_power_series Γ R x).coeff n = power_series.coeff R n x :=
 by simp
 
+@[simp] lemma of_power_series_C (r : R) :
+  of_power_series Γ R (power_series.C R r) = hahn_series.C r :=
+begin
+  ext n,
+  simp only [C, single_coeff, of_power_series_apply, ring_hom.coe_mk],
+  split_ifs with hn hn,
+  { rw hn,
+    convert @emb_domain_coeff _ _ _ _ _ _ _ _ 0,
+    simp },
+  { rw emb_domain_notin_image_support,
+    simp only [not_exists, set.mem_image, to_power_series_symm_apply_coeff, mem_support,
+               power_series.coeff_C],
+    intro,
+    simp [ne.symm hn] {contextual := tt} }
+end
+
+@[simp] lemma of_power_series_X :
+  of_power_series Γ R power_series.X = single 1 1 :=
+begin
+  ext n,
+  simp only [single_coeff, of_power_series_apply, ring_hom.coe_mk],
+  split_ifs with hn hn,
+  { rw hn,
+    convert @emb_domain_coeff _ _ _ _ _ _ _ _ 1;
+    simp },
+  { rw emb_domain_notin_image_support,
+    simp only [not_exists, set.mem_image, to_power_series_symm_apply_coeff, mem_support,
+               power_series.coeff_X],
+    intro,
+    simp [ne.symm hn] {contextual := tt} }
+end
+
+@[simp] lemma of_power_series_X_pow {R} [comm_semiring R] (n : ℕ) :
+  of_power_series Γ R (power_series.X ^ n) = single (n : Γ) 1 :=
+begin
+  rw ring_hom.map_pow,
+  induction n with n ih,
+  { refl },
+  rw [pow_succ, ih, of_power_series_X, mul_comm, single_mul_single, one_mul, nat.cast_succ]
+end
+
 end semiring
 
 section algebra

src/ring_theory/laurent_series.lean

@@ -99,49 +99,8 @@ begin
     coe_power_series],
 end
 
-@[simp] lemma of_power_series_C (r : R) :
-  of_power_series ℤ R (power_series.C R r) = hahn_series.C r :=
-begin
-  ext n,
-  simp only [C, single_coeff, of_power_series_apply, ring_hom.coe_mk],
-  split_ifs with hn hn,
-  { rw [hn, ←int.coe_nat_zero],
-    convert @emb_domain_coeff _ _ _ _ _ _ _ _ 0,
-    simp },
-  { rw emb_domain_notin_image_support,
-    simp only [not_exists, set.mem_image, to_power_series_symm_apply_coeff, mem_support,
-               power_series.coeff_C],
-    intro,
-    simp [ne.symm hn] {contextual := tt} }
-end
-
-@[simp] lemma of_power_series_X :
-  of_power_series ℤ R power_series.X = single 1 1 :=
-begin
-  ext n,
-  simp only [single_coeff, of_power_series_apply, ring_hom.coe_mk],
-  split_ifs with hn hn,
-  { rw [hn, ←int.coe_nat_one],
-    convert @emb_domain_coeff _ _ _ _ _ _ _ _ 1,
-    simp },
-  { rw emb_domain_notin_image_support,
-    simp only [not_exists, set.mem_image, to_power_series_symm_apply_coeff, mem_support,
-               power_series.coeff_X],
-    intro,
-    simp [ne.symm hn] {contextual := tt} }
-end
-
 end semiring
 
-@[simp] lemma of_power_series_X_pow [comm_semiring R] (n : ℕ) :
-  of_power_series ℤ R (power_series.X ^ n) = single (n : ℤ) 1 :=
-begin
-  rw ring_hom.map_pow,
-  induction n with n ih,
-  { refl },
-  rw [pow_succ, int.coe_nat_succ, ih, of_power_series_X, mul_comm, single_mul_single, one_mul],
-end
-
 instance [comm_semiring R] : algebra (power_series R) (laurent_series R) :=
 (hahn_series.of_power_series ℤ R).to_algebra
 
@@ -163,13 +122,14 @@ rfl
     by_cases h : 0 ≤ z.order,
     { refine ⟨⟨power_series.X ^ (int.nat_abs z.order) * power_series_part z, 1⟩, _⟩,
       simp only [ring_hom.map_one, mul_one, ring_hom.map_mul, coe_algebra_map,
-        of_power_series_X_pow, submonoid.coe_one],
+        of_power_series_X_pow, submonoid.coe_one, int.nat_cast_eq_coe_nat],
       rw [int.nat_abs_of_nonneg h, ← coe_power_series, single_order_mul_power_series_part] },
     { refine ⟨⟨power_series_part z, power_series.X ^ (int.nat_abs z.order), ⟨_, rfl⟩⟩, _⟩,
       simp only [coe_algebra_map, of_power_series_power_series_part],
       rw [mul_comm _ z],
       refine congr rfl _,
-      rw [subtype.coe_mk, of_power_series_X_pow, int.of_nat_nat_abs_of_nonpos],
+      rw [subtype.coe_mk, of_power_series_X_pow,
+          int.nat_cast_eq_coe_nat, int.of_nat_nat_abs_of_nonpos],
       exact le_of_not_ge h } end),
   eq_iff_exists := (begin intros x y,
     rw [coe_algebra_map, of_power_series_injective.eq_iff],
@@ -194,57 +154,59 @@ is_localization.of_le (submonoid.powers (power_series.X : power_series K)) _
 
 end laurent_series
 
-namespace polynomial
-
-section laurent_series
-
-variables [comm_semiring R] (p q : polynomial R)
-
-open polynomial laurent_series hahn_series
+namespace power_series
 
-lemma coe_laurent : (p : laurent_series R) = of_power_series ℤ R p := rfl
+open laurent_series
 
-@[norm_cast] lemma coe_coe : ((p : power_series R) : laurent_series R) = p := rfl
+variables [semiring R] (f g : power_series R)
 
-@[simp] lemma coe_laurent_zero : ((0 : polynomial R) : laurent_series R) = 0 :=
-by rw [coe_laurent, coe_zero, _root_.map_zero]
+@[simp, norm_cast] lemma coe_zero : ((0 : power_series R) : laurent_series R) = 0 :=
+(of_power_series ℤ R).map_zero
 
-@[simp] lemma coe_laurent_one : ((1 : polynomial R) : laurent_series R) = 1 :=
-by rw [coe_laurent, coe_one, _root_.map_one]
+@[simp, norm_cast] lemma coe_one : ((1 : power_series R) : laurent_series R) = 1 :=
+(of_power_series ℤ R).map_one
 
-@[norm_cast] lemma coe_laurent_add : ((p + q : polynomial R) : laurent_series R) = p + q :=
-by rw [coe_laurent, coe_add, _root_.map_add, ←coe_laurent, ←coe_laurent]
+@[simp, norm_cast] lemma coe_add : ((f + g : power_series R) : laurent_series R) = f + g :=
+(of_power_series ℤ R).map_add _ _
 
-@[norm_cast] lemma coe_laurent_mul : ((p * q : polynomial R) : laurent_series R) = p * q :=
-by rw [coe_laurent, coe_mul, _root_.map_mul, ←coe_laurent, ←coe_laurent]
+@[simp, norm_cast] lemma coe_mul : ((f * g : power_series R) : laurent_series R) = f * g :=
+(of_power_series ℤ R).map_mul _ _
 
-@[norm_cast] lemma coeff_coe_laurent_coe (i : ℕ) :
-  ((p : polynomial R) : laurent_series R).coeff i = p.coeff i :=
-by rw [←coe_coe, coeff_coe_power_series, coeff_coe]
-
-lemma coeff_coe_laurent (i : ℤ) :
-  ((p : polynomial R) : laurent_series R).coeff i = if i < 0 then 0 else p.coeff i.nat_abs :=
+lemma coeff_coe (i : ℤ) :
+  ((f : power_series R) : laurent_series R).coeff i =
+    if i < 0 then 0 else power_series.coeff R i.nat_abs f :=
 begin
   cases i,
-  { rw [int.nat_abs_of_nat_core, int.of_nat_eq_coe, coeff_coe_laurent_coe,
+  { rw [int.nat_abs_of_nat_core, int.of_nat_eq_coe, coeff_coe_power_series,
         if_neg (int.coe_nat_nonneg _).not_lt] },
-  { rw [coe_laurent, of_power_series_apply, emb_domain_notin_image_support,
+  { rw [coe_power_series, of_power_series_apply, emb_domain_notin_image_support,
         if_pos (int.neg_succ_lt_zero _)],
-    simp only [not_exists, rel_embedding.coe_fn_mk, set.mem_image, not_and, coeff_coe,
+    simp only [not_exists, rel_embedding.coe_fn_mk, set.mem_image, not_and,
                function.embedding.coe_fn_mk, ne.def, to_power_series_symm_apply_coeff, mem_support,
                int.nat_cast_eq_coe_nat, int.coe_nat_eq, implies_true_iff, not_false_iff] }
 end
 
-@[simp] lemma coe_laurent_C (r : R) : ((C r : polynomial R) : laurent_series R) = hahn_series.C r :=
-by rw [coe_laurent, coe_C, of_power_series_C]
+@[simp, norm_cast] lemma coe_C (r : R) : ((C R r : power_series R) : laurent_series R) =
+  hahn_series.C r :=
+of_power_series_C _
 
-@[simp] lemma coe_laurent_X : ((X : polynomial R) : laurent_series R) = single 1 1 :=
-by rw [coe_laurent, coe_X, of_power_series_X]
+@[simp] lemma coe_X : ((X : power_series R) : laurent_series R) = single 1 1 :=
+of_power_series_X
 
-@[norm_cast] lemma coe_laurent_smul (r : R) :
-  ((r • p : polynomial R) : laurent_series R) = r • p :=
-by rw [smul_eq_C_mul, coe_laurent_mul, coe_laurent_C, C_mul_eq_smul]
+@[simp, norm_cast] lemma coe_smul {S : Type*} [semiring S] [module R S]
+  (r : R) (x : power_series S) : ((r • x : power_series S) : laurent_series S) = r • x :=
+by { ext, simp [coeff_coe, coeff_smul, smul_ite] }
 
-end laurent_series
+@[simp, norm_cast] lemma coe_bit0 :
+  ((bit0 f : power_series R) : laurent_series R) = bit0 f :=
+(of_power_series ℤ R).map_bit0 _
+
+@[simp, norm_cast] lemma coe_bit1 :
+  ((bit1 f : power_series R) : laurent_series R) = bit1 f :=
+(of_power_series ℤ R).map_bit1 _
+
+@[simp, norm_cast] lemma coe_pow (n : ℕ) :
+  ((f ^ n : power_series R) : laurent_series R) = f ^ n :=
+(of_power_series ℤ R).map_pow _ _
 
-end polynomial
+end power_series

src/ring_theory/power_series/basic.lean

@@ -1045,8 +1045,8 @@ mv_power_series.coeff_mul_C _ φ a
   coeff R n (C R a * φ) = a * coeff R n φ :=
 mv_power_series.coeff_C_mul _ φ a
 
-@[simp] lemma coeff_smul (n : ℕ) (φ : power_series R) (a : R) :
-  coeff R n (a • φ) = a * coeff R n φ :=
+@[simp] lemma coeff_smul {S : Type*} [semiring S] [module R S]
+  (n : ℕ) (φ : power_series S) (a : R) : coeff S n (a • φ) = a • coeff S n φ :=
 rfl
 
 @[simp] lemma coeff_succ_mul_X (n : ℕ) (φ : power_series R) :