Documentation

Mathlib.RingTheory.PowerSeries.WellKnown

Definition of well-known power series #

In this file we define the following power series:

def PowerSeries.invUnitsSub {R : Type u_1} [Ring R] (u : Rˣ) :

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

Equations
Instances For
    @[simp]
    theorem PowerSeries.coeff_invUnitsSub {R : Type u_1} [Ring R] (u : Rˣ) (n : ) :
    @[simp]
    theorem PowerSeries.invUnitsSub_mul_X {R : Type u_1} [Ring R] (u : Rˣ) :
    @[simp]
    theorem PowerSeries.invUnitsSub_mul_sub {R : Type u_1} [Ring R] (u : Rˣ) :
    PowerSeries.invUnitsSub u * ((PowerSeries.C R) u - PowerSeries.X) = 1
    def PowerSeries.exp (A : Type u_1) [Ring A] [Algebra A] :

    Power series for the exponential function at zero.

    Equations
    Instances For
      def PowerSeries.sin (A : Type u_1) [Ring A] [Algebra A] :

      Power series for the sine function at zero.

      Equations
      Instances For
        def PowerSeries.cos (A : Type u_1) [Ring A] [Algebra A] :

        Power series for the cosine function at zero.

        Equations
        Instances For
          @[simp]
          theorem PowerSeries.coeff_exp {A : Type u_1} [Ring A] [Algebra A] (n : ) :
          @[simp]
          theorem PowerSeries.coeff_sin_bit0 {A : Type u_1} [Ring A] [Algebra A] (n : ) :
          @[simp]
          @[simp]
          @[simp]
          theorem PowerSeries.coeff_cos_bit1 {A : Type u_1} [Ring A] [Algebra A] (n : ) :
          @[simp]
          theorem PowerSeries.map_exp {A : Type u_1} {A' : Type u_2} [Ring A] [Ring A'] [Algebra A] [Algebra A'] (f : A →+* A') :
          @[simp]
          theorem PowerSeries.map_sin {A : Type u_1} {A' : Type u_2} [Ring A] [Ring A'] [Algebra A] [Algebra A'] (f : A →+* A') :
          @[simp]
          theorem PowerSeries.map_cos {A : Type u_1} {A' : Type u_2} [Ring A] [Ring A'] [Algebra A] [Algebra A'] (f : A →+* A') :

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

          theorem PowerSeries.exp_mul_exp_neg_eq_one {A : Type u_1} [CommRing A] [Algebra A] :
          PowerSeries.exp A * PowerSeries.evalNegHom (PowerSeries.exp A) = 1

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

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

          theorem PowerSeries.exp_pow_sum {A : Type u_1} [CommRing A] [Algebra A] (n : ) :
          (Finset.sum (Finset.range n) fun (k : ) => PowerSeries.exp A ^ k) = PowerSeries.mk fun (p : ) => Finset.sum (Finset.range n) fun (k : ) => k ^ p * (algebraMap A) ((Nat.factorial p))⁻¹

          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$.