feat(ring_theory/power_series): define power series for exp, sin,…

… `cos`, and `1 / (u - x)`. (#5432)

This PR defines `power_series.exp` etc to be formal power series for the corresponding functions. Once we have a bridge to `is_analytic`, we should redefine `complex.exp` etc using these power series.

src/algebra/field.lean

@@ -243,7 +243,7 @@ variables {β γ : Type*} [division_ring α] [semiring β] [nontrivial β] [divi
 
 lemma map_ne_zero : f x ≠ 0 ↔ x ≠ 0 := f.to_monoid_with_zero_hom.map_ne_zero
 
-lemma map_eq_zero : f x = 0 ↔ x = 0 := f.to_monoid_with_zero_hom.map_eq_zero
+@[simp] lemma map_eq_zero : f x = 0 ↔ x = 0 := f.to_monoid_with_zero_hom.map_eq_zero
 
 variables (x y)
 

src/algebra/group/units_hom.lean

@@ -24,6 +24,10 @@ monoid_hom.mk'
 
 @[simp, to_additive] lemma coe_map (f : M →* N) (x : units M) : ↑(map f x) = f x := rfl
 
+@[simp, to_additive] lemma coe_map_inv (f : M →* N) (u : units M) :
+  ↑(map f u)⁻¹ = f ↑u⁻¹ :=
+rfl
+
 @[simp, to_additive]
 lemma map_comp (f : M →* N) (g : N →* P) : map (g.comp f) = (map g).comp (map f) := rfl
 

src/analysis/calculus/formal_multilinear_series.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Sébastien Gouëzel
 -/
 import analysis.normed_space.multilinear
-import ring_theory.power_series
+import ring_theory.power_series.basic
 
 /-!
 # Formal multilinear series

src/data/complex/is_R_or_C.lean

@@ -187,8 +187,8 @@ lemma conj_bijective : @function.bijective K K is_R_or_C.conj := conj_involutive
 
 lemma conj_inj (z w : K) : conj z = conj w ↔ z = w := conj_bijective.1.eq_iff
 
-@[simp] lemma conj_eq_zero {z : K} : conj z = 0 ↔ z = 0 :=
-by simpa using @conj_inj K _ z 0
+lemma conj_eq_zero {z : K} : conj z = 0 ↔ z = 0 :=
+ring_hom.map_eq_zero conj
 
 lemma eq_conj_iff_real {z : K} : conj z = z ↔ ∃ r : ℝ, z = (r : K) :=
 begin

src/ring_theory/power_series.lean → src/ring_theory/power_series/basic.lean

@@ -676,10 +676,12 @@ lemma inv_eq_zero {φ : mv_power_series σ k} :
  λ h, ext $ λ n, by { rw coeff_inv, split_ifs;
  simp only [h, mv_power_series.coeff_zero, zero_mul, inv_zero, neg_zero] }⟩
 
-@[simp, priority 1100] lemma inv_of_unit_eq (φ : mv_power_series σ k) (h : constant_coeff σ k φ ≠ 0) :
+@[simp, priority 1100]
+lemma inv_of_unit_eq (φ : mv_power_series σ k) (h : constant_coeff σ k φ ≠ 0) :
   inv_of_unit φ (units.mk0 _ h) = φ⁻¹ := rfl
 
-@[simp] lemma inv_of_unit_eq' (φ : mv_power_series σ k) (u : units k) (h : constant_coeff σ k φ = u) :
+@[simp]
+lemma inv_of_unit_eq' (φ : mv_power_series σ k) (u : units k) (h : constant_coeff σ k φ = u) :
   inv_of_unit φ u = φ⁻¹ :=
 begin
   rw ← inv_of_unit_eq φ (h.symm ▸ u.ne_zero),

src/ring_theory/power_series/well_known.lean

@@ -0,0 +1,84 @@
+/-
+Copyright (c) 2020 Yury G. Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Yury G. Kudryashov
+-/
+import ring_theory.power_series.basic
+import data.nat.parity
+
+/-!
+# Definition of well-known power series
+
+In this file we define the following power series:
+
+* `power_series.inv_units_sub`: given `u : units R`, this is the series for `1 / (u - x)`.
+  It is given by `∑ n, x ^ n /ₚ u ^ (n + 1)`.
+
+* `power_series.sin`, `power_series.cos`, `power_series.exp` : power series for sin, cosine, and
+  exponential functions.
+-/
+
+namespace power_series
+
+section ring
+
+variables {R S : Type*} [ring R] [ring S]
+
+/-- The power series for `1 / (u - x)`. -/
+def inv_units_sub (u : units R) : power_series R := mk $ λ n, 1 /ₚ u ^ (n + 1)
+
+@[simp] lemma coeff_inv_units_sub (u : units R) (n : ℕ) :
+  coeff R n (inv_units_sub u) = 1 /ₚ u ^ (n + 1) :=
+coeff_mk _ _
+
+@[simp] lemma constant_coeff_inv_units_sub (u : units R) :
+  constant_coeff R (inv_units_sub u) = 1 /ₚ u :=
+by rw [← coeff_zero_eq_constant_coeff_apply, coeff_inv_units_sub, zero_add, pow_one]
+
+@[simp] lemma inv_units_sub_mul_X (u : units R) :
+  inv_units_sub u * X = inv_units_sub u * C R u - 1 :=
+begin
+  ext (_|n),
+  { simp },
+  { simp [n.succ_ne_zero, pow_succ] }
+end
+
+@[simp] lemma inv_units_sub_mul_sub (u : units R) : inv_units_sub u * (C R u - X) = 1 :=
+by simp [mul_sub, sub_sub_cancel]
+
+lemma map_inv_units_sub (f : R →+* S) (u : units R) :
+  map f (inv_units_sub u) = inv_units_sub (units.map (f : R →* S) u) :=
+by { ext, simp [← monoid_hom.map_pow] }
+
+end ring
+
+section field
+
+variables (k k' : Type*) [field k] [field k']
+
+open_locale nat
+
+/-- Power series for the exponential function at zero. -/
+def exp : power_series k := mk $ λ n, 1 / n!
+
+/-- Power series for the sine function at zero. -/
+def sin : power_series k :=
+mk $ λ n, if even n then 0 else (-1) ^ (n / 2) / n!
+
+/-- Power series for the cosine function at zero. -/
+def cos : power_series k :=
+mk $ λ n, if even n then (-1) ^ (n / 2) / n! else 0
+
+variables {k k'} (n : ℕ) (f : k →+* k')
+
+@[simp] lemma coeff_exp : coeff k n (exp k) = 1 / n! := coeff_mk _ _
+
+@[simp] lemma map_exp : map f (exp k) = exp k' := by { ext, simp [f.map_inv] }
+
+@[simp] lemma map_sin : map f (sin k) = sin k' := by { ext, simp [sin, apply_ite f, f.map_div] }
+
+@[simp] lemma map_cos : map f (cos k) = cos k' := by { ext, simp [cos, apply_ite f, f.map_div] }
+
+end field
+
+end power_series