# mathlibdocumentation

ring_theory.power_series.well_known

# Definition of well-known power series #

In this file we define the following power series:

• power_series.inv_units_sub: given u : 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.

def power_series.inv_units_sub {R : Type u_1} [ring R] (u : Rˣ) :

The power series for 1 / (u - x).

Equations
@[simp]
theorem power_series.coeff_inv_units_sub {R : Type u_1} [ring R] (u : Rˣ) (n : ) :
= 1 /ₚ u ^ (n + 1)
@[simp]
theorem power_series.constant_coeff_inv_units_sub {R : Type u_1} [ring R] (u : Rˣ) :
@[simp]
theorem power_series.inv_units_sub_mul_X {R : Type u_1} [ring R] (u : Rˣ) :
@[simp]
theorem power_series.inv_units_sub_mul_sub {R : Type u_1} [ring R] (u : Rˣ) :
= 1
theorem power_series.map_inv_units_sub {R : Type u_1} {S : Type u_2} [ring R] [ring S] (f : R →+* S) (u : Rˣ) :
def power_series.exp (A : Type u_1) [ring A] [ A] :

Power series for the exponential function at zero.

Equations
def power_series.sin (A : Type u_1) [ring A] [ A] :

Power series for the sine function at zero.

Equations
def power_series.cos (A : Type u_1) [ring A] [ A] :

Power series for the cosine function at zero.

Equations
@[simp]
theorem power_series.coeff_exp {A : Type u_1} [ring A] [ A] (n : ) :
n) = A) (1 / (n.factorial))
@[simp]
theorem power_series.constant_coeff_exp {A : Type u_1} [ring A] [ A] :
@[simp]
theorem power_series.coeff_sin_bit0 {A : Type u_1} [ring A] [ A] (n : ) :
(bit0 n)) = 0
@[simp]
theorem power_series.coeff_sin_bit1 {A : Type u_1} [ring A] [ A] (n : ) :
(bit1 n)) = (-1) ^ n * (bit1 n))
@[simp]
theorem power_series.coeff_cos_bit0 {A : Type u_1} [ring A] [ A] (n : ) :
(bit0 n)) = (-1) ^ n * (bit0 n))
@[simp]
theorem power_series.coeff_cos_bit1 {A : Type u_1} [ring A] [ A] (n : ) :
(bit1 n)) = 0
@[simp]
theorem power_series.map_exp {A : Type u_1} {A' : Type u_2} [ring A] [ring A'] [ A] [ A'] (f : A →+* A') :
@[simp]
theorem power_series.map_sin {A : Type u_1} {A' : Type u_2} [ring A] [ring A'] [ A] [ A'] (f : A →+* A') :
@[simp]
theorem power_series.map_cos {A : Type u_1} {A' : Type u_2} [ring A] [ring A'] [ A] [ A'] (f : A →+* A') :
theorem power_series.exp_mul_exp_eq_exp_add {A : Type u_1} [comm_ring A] [ A] (a b : A) :

Shows that $e^{aX} * e^{bX} = e^{(a + b)X}$

theorem power_series.exp_mul_exp_neg_eq_one {A : Type u_1} [comm_ring A] [ A] :

Shows that $e^{x} * e^{-x} = 1$

theorem power_series.exp_pow_eq_rescale_exp {A : Type u_1} [comm_ring A] [ A] (k : ) :
=

Shows that $(e^{X})^k = e^{kX}$.

theorem power_series.exp_pow_sum {A : Type u_1} [comm_ring A] [ A] (n : ) :
(finset.range n).sum (λ (k : ), = power_series.mk (λ (p : ), (finset.range n).sum (λ (k : ), k ^ p * A) ((p.factorial))⁻¹))

Shows that $\sum_{k = 0}^{n - 1} (e^{X})^k = \sum_{p = 0}^{\infty} \sum_{k = 0}^{n - 1} \frac{k^p}{p!}X^p$.