theorem PowerSeries.derivative_logbar.{u_1}
  {KType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [CommRingCommRing.{u} (α : Type u) : Type uA commutative ring is a ring with commutative multiplication.  KType u_1]
  [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 ℚRat : TypeRational numbers, implemented as a pair of integers `num / den` such that the
denominator is positive and the numerator and denominator are coprime.
 KType u_1] :
  (PowerSeries.derivativePowerSeries.derivative.{u_1} (R : Type u_1) [CommSemiring R] : Derivation R (PowerSeries R) (PowerSeries R)The formal derivative of a formal power series  KType u_1)
      (PowerSeries.logbarPowerSeries.logbar.{u_1} (K : Type u_1) [CommRing K] [Algebra ℚ K] : PowerSeries KThe logarithm series `logbar = ∑_{n≥1} (-1)^{n-1}/n · x^n`, which is the Mercator series
for `log(1+x)`. This is `\overline{\log}` in Definition 7.8.2 (def.fps.exp-log).  KType u_1) =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
    PowerSeries.invOnePlusXPowerSeries.invOnePlusX.{u_1} (K : Type u_1) [CommRing K] [Algebra ℚ K] : PowerSeries KThe series `(1+x)⁻¹ = ∑_{n≥0} (-1)^n x^n`.  KType u_1

theorem PowerSeries.derivative_expbar.{u_1}
  {KType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [CommRingCommRing.{u} (α : Type u) : Type uA commutative ring is a ring with commutative multiplication.  KType u_1]
  [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 ℚRat : TypeRational numbers, implemented as a pair of integers `num / den` such that the
denominator is positive and the numerator and denominator are coprime.
 KType u_1] :
  (PowerSeries.derivativePowerSeries.derivative.{u_1} (R : Type u_1) [CommSemiring R] : Derivation R (PowerSeries R) (PowerSeries R)The formal derivative of a formal power series  KType u_1)
      (PowerSeries.expbarPowerSeries.expbar.{u_1} (K : Type u_1) [CommRing K] [Algebra ℚ K] : PowerSeries KThe shifted exponential series `expbar = exp - 1 = ∑_{n≥1} 1/n! · x^n`.
This is `\overline{\exp}` in Definition 7.8.2 (def.fps.exp-log).  KType u_1) =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
    PowerSeries.expPowerSeries.exp.{u_1} (A : Type u_1) [Ring A] [Algebra ℚ A] : PowerSeries APower series for the exponential function at zero.  KType u_1

theorem PowerSeries.invOnePlusX_subst_eq_inv.{u_2}
  {KType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [FieldField.{u} (K : Type u) : Type uA `Field` is a `CommRing` with multiplicative inverses for nonzero elements.

An instance of `Field K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance].

If the field has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  KType u_2] [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 ℚRat : TypeRational numbers, implemented as a pair of integers `num / den` such that the
denominator is positive and the numerator and denominator are coprime.
 KType u_2]
  {gPowerSeries K : PowerSeriesPowerSeries.{u_1} (R : Type u_1) : Type u_1Formal power series over a coefficient type `R`  KType u_2}
  (hgPowerSeries.constantCoeff g = 0 : PowerSeries.constantCoeffPowerSeries.constantCoeff.{u_1} {R : Type u_1} [Semiring R] : PowerSeries R →+* RThe constant coefficient of a formal power series.  gPowerSeries K =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. 0) :
  PowerSeries.substPowerSeries.subst.{u_2, u_3, u_4} {R : Type u_2} [CommRing R] {τ : Type u_3} {S : Type u_4} [CommRing S] [Algebra R S]
  (a : MvPowerSeries τ S) (f : PowerSeries R) : MvPowerSeries τ SSubstitution of power series into a power series.  gPowerSeries K
      (PowerSeries.invOnePlusXPowerSeries.invOnePlusX.{u_1} (K : Type u_1) [CommRing K] [Algebra ℚ K] : PowerSeries KThe series `(1+x)⁻¹ = ∑_{n≥0} (-1)^n x^n`.  KType u_2) =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
    (HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`.1 +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`. gPowerSeries K)HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`.⁻¹Inv.inv.{u} {α : Type u} [self : Inv α] : α → α`a⁻¹` computes the inverse of `a`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `⁻¹` in identifiers is `inv`.

theorem PowerSeries.derivative_exp_comp.{u_1}
  {KType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [CommRingCommRing.{u} (α : Type u) : Type uA commutative ring is a ring with commutative multiplication.  KType u_1]
  [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 ℚRat : TypeRational numbers, implemented as a pair of integers `num / den` such that the
denominator is positive and the numerator and denominator are coprime.
 KType u_1] {gPowerSeries K : PowerSeriesPowerSeries.{u_1} (R : Type u_1) : Type u_1Formal power series over a coefficient type `R`  KType u_1}
  (hgPowerSeries.constantCoeff g = 0 : PowerSeries.constantCoeffPowerSeries.constantCoeff.{u_1} {R : Type u_1} [Semiring R] : PowerSeries R →+* RThe constant coefficient of a formal power series.  gPowerSeries K =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. 0) :
  (PowerSeries.derivativePowerSeries.derivative.{u_1} (R : Type u_1) [CommSemiring R] : Derivation R (PowerSeries R) (PowerSeries R)The formal derivative of a formal power series  KType u_1)
      (PowerSeries.substPowerSeries.subst.{u_2, u_3, u_4} {R : Type u_2} [CommRing R] {τ : Type u_3} {S : Type u_4} [CommRing S] [Algebra R S]
  (a : MvPowerSeries τ S) (f : PowerSeries R) : MvPowerSeries τ SSubstitution of power series into a power series.  gPowerSeries K
        (PowerSeries.expPowerSeries.exp.{u_1} (A : Type u_1) [Ring A] [Algebra ℚ A] : PowerSeries APower series for the exponential function at zero.  KType u_1)) =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
    PowerSeries.substPowerSeries.subst.{u_2, u_3, u_4} {R : Type u_2} [CommRing R] {τ : Type u_3} {S : Type u_4} [CommRing S] [Algebra R S]
  (a : MvPowerSeries τ S) (f : PowerSeries R) : MvPowerSeries τ SSubstitution of power series into a power series.  gPowerSeries K
        (PowerSeries.expPowerSeries.exp.{u_1} (A : Type u_1) [Ring A] [Algebra ℚ A] : PowerSeries APower series for the exponential function at zero.  KType u_1) *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`.
      (PowerSeries.derivativePowerSeries.derivative.{u_1} (R : Type u_1) [CommSemiring R] : Derivation R (PowerSeries R) (PowerSeries R)The formal derivative of a formal power series  KType u_1) gPowerSeries K

theorem PowerSeries.derivative_expbar_comp.{u_1}
  {KType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [CommRingCommRing.{u} (α : Type u) : Type uA commutative ring is a ring with commutative multiplication.  KType u_1]
  [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 ℚRat : TypeRational numbers, implemented as a pair of integers `num / den` such that the
denominator is positive and the numerator and denominator are coprime.
 KType u_1] {gPowerSeries K : PowerSeriesPowerSeries.{u_1} (R : Type u_1) : Type u_1Formal power series over a coefficient type `R`  KType u_1}
  (hgPowerSeries.constantCoeff g = 0 : PowerSeries.constantCoeffPowerSeries.constantCoeff.{u_1} {R : Type u_1} [Semiring R] : PowerSeries R →+* RThe constant coefficient of a formal power series.  gPowerSeries K =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. 0) :
  (PowerSeries.derivativePowerSeries.derivative.{u_1} (R : Type u_1) [CommSemiring R] : Derivation R (PowerSeries R) (PowerSeries R)The formal derivative of a formal power series  KType u_1)
      (PowerSeries.substPowerSeries.subst.{u_2, u_3, u_4} {R : Type u_2} [CommRing R] {τ : Type u_3} {S : Type u_4} [CommRing S] [Algebra R S]
  (a : MvPowerSeries τ S) (f : PowerSeries R) : MvPowerSeries τ SSubstitution of power series into a power series.  gPowerSeries K
        (PowerSeries.expbarPowerSeries.expbar.{u_1} (K : Type u_1) [CommRing K] [Algebra ℚ K] : PowerSeries KThe shifted exponential series `expbar = exp - 1 = ∑_{n≥1} 1/n! · x^n`.
This is `\overline{\exp}` in Definition 7.8.2 (def.fps.exp-log).  KType u_1)) =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
    PowerSeries.substPowerSeries.subst.{u_2, u_3, u_4} {R : Type u_2} [CommRing R] {τ : Type u_3} {S : Type u_4} [CommRing S] [Algebra R S]
  (a : MvPowerSeries τ S) (f : PowerSeries R) : MvPowerSeries τ SSubstitution of power series into a power series.  gPowerSeries K
        (PowerSeries.expPowerSeries.exp.{u_1} (A : Type u_1) [Ring A] [Algebra ℚ A] : PowerSeries APower series for the exponential function at zero.  KType u_1) *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`.
      (PowerSeries.derivativePowerSeries.derivative.{u_1} (R : Type u_1) [CommSemiring R] : Derivation R (PowerSeries R) (PowerSeries R)The formal derivative of a formal power series  KType u_1) gPowerSeries K

theorem PowerSeries.derivative_logbar_comp.{u_2}
  {KType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [FieldField.{u} (K : Type u) : Type uA `Field` is a `CommRing` with multiplicative inverses for nonzero elements.

An instance of `Field K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance].

If the field has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  KType u_2] [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 ℚRat : TypeRational numbers, implemented as a pair of integers `num / den` such that the
denominator is positive and the numerator and denominator are coprime.
 KType u_2]
  {gPowerSeries K : PowerSeriesPowerSeries.{u_1} (R : Type u_1) : Type u_1Formal power series over a coefficient type `R`  KType u_2}
  (hgPowerSeries.constantCoeff g = 0 : PowerSeries.constantCoeffPowerSeries.constantCoeff.{u_1} {R : Type u_1} [Semiring R] : PowerSeries R →+* RThe constant coefficient of a formal power series.  gPowerSeries K =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. 0) :
  (PowerSeries.derivativePowerSeries.derivative.{u_1} (R : Type u_1) [CommSemiring R] : Derivation R (PowerSeries R) (PowerSeries R)The formal derivative of a formal power series  KType u_2)
      (PowerSeries.substPowerSeries.subst.{u_2, u_3, u_4} {R : Type u_2} [CommRing R] {τ : Type u_3} {S : Type u_4} [CommRing S] [Algebra R S]
  (a : MvPowerSeries τ S) (f : PowerSeries R) : MvPowerSeries τ SSubstitution of power series into a power series.  gPowerSeries K
        (PowerSeries.logbarPowerSeries.logbar.{u_1} (K : Type u_1) [CommRing K] [Algebra ℚ K] : PowerSeries KThe logarithm series `logbar = ∑_{n≥1} (-1)^{n-1}/n · x^n`, which is the Mercator series
for `log(1+x)`. This is `\overline{\log}` in Definition 7.8.2 (def.fps.exp-log).  KType u_2)) =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
    (HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`.1 +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`. gPowerSeries K)HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`.⁻¹Inv.inv.{u} {α : Type u} [self : Inv α] : α → α`a⁻¹` computes the inverse of `a`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `⁻¹` in identifiers is `inv`. *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`.
      (PowerSeries.derivativePowerSeries.derivative.{u_1} (R : Type u_1) [CommSemiring R] : Derivation R (PowerSeries R) (PowerSeries R)The formal derivative of a formal power series  KType u_2) gPowerSeries K

theorem PowerSeries.eq_of_derivative_eq_mul_of_inv.{u_1}
  {KType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [CommRingCommRing.{u} (α : Type u) : Type uA commutative ring is a ring with commutative multiplication.  KType u_1]
  [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 ℚRat : TypeRational numbers, implemented as a pair of integers `num / den` such that the
denominator is positive and the numerator and denominator are coprime.
 KType u_1] {h₁PowerSeries K h₂PowerSeries K gPowerSeries K : PowerSeriesPowerSeries.{u_1} (R : Type u_1) : Type u_1Formal power series over a coefficient type `R`  KType u_1}
  (hd₁(PowerSeries.derivative K) h₁ = (1 + h₁) * g :
    (PowerSeries.derivativePowerSeries.derivative.{u_1} (R : Type u_1) [CommSemiring R] : Derivation R (PowerSeries R) (PowerSeries R)The formal derivative of a formal power series  KType u_1) h₁PowerSeries K =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
      (HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`.1 +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`. h₁PowerSeries K)HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`. *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`. gPowerSeries K)
  (hd₂(PowerSeries.derivative K) h₂ = (1 + h₂) * g :
    (PowerSeries.derivativePowerSeries.derivative.{u_1} (R : Type u_1) [CommSemiring R] : Derivation R (PowerSeries R) (PowerSeries R)The formal derivative of a formal power series  KType u_1) h₂PowerSeries K =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
      (HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`.1 +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`. h₂PowerSeries K)HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`. *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`. gPowerSeries K)
  (hcPowerSeries.constantCoeff h₁ = PowerSeries.constantCoeff h₂ :
    PowerSeries.constantCoeffPowerSeries.constantCoeff.{u_1} {R : Type u_1} [Semiring R] : PowerSeries R →+* RThe constant coefficient of a formal power series.  h₁PowerSeries K =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
      PowerSeries.constantCoeffPowerSeries.constantCoeff.{u_1} {R : Type u_1} [Semiring R] : PowerSeries R →+* RThe constant coefficient of a formal power series.  h₂PowerSeries K) :
  h₁PowerSeries K =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. h₂PowerSeries K

theorem PowerSeries.eq_of_derivative_eq_one.{u_1}
  {KType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [CommRingCommRing.{u} (α : Type u) : Type uA commutative ring is a ring with commutative multiplication.  KType u_1]
  [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 ℚRat : TypeRational numbers, implemented as a pair of integers `num / den` such that the
denominator is positive and the numerator and denominator are coprime.
 KType u_1] {h₁PowerSeries K h₂PowerSeries K : PowerSeriesPowerSeries.{u_1} (R : Type u_1) : Type u_1Formal power series over a coefficient type `R`  KType u_1}
  (hd₁(PowerSeries.derivative K) h₁ = 1 :
    (PowerSeries.derivativePowerSeries.derivative.{u_1} (R : Type u_1) [CommSemiring R] : Derivation R (PowerSeries R) (PowerSeries R)The formal derivative of a formal power series  KType u_1) h₁PowerSeries K =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. 1)
  (hd₂(PowerSeries.derivative K) h₂ = 1 :
    (PowerSeries.derivativePowerSeries.derivative.{u_1} (R : Type u_1) [CommSemiring R] : Derivation R (PowerSeries R) (PowerSeries R)The formal derivative of a formal power series  KType u_1) h₂PowerSeries K =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. 1)
  (hcPowerSeries.constantCoeff h₁ = PowerSeries.constantCoeff h₂ :
    PowerSeries.constantCoeffPowerSeries.constantCoeff.{u_1} {R : Type u_1} [Semiring R] : PowerSeries R →+* RThe constant coefficient of a formal power series.  h₁PowerSeries K =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
      PowerSeries.constantCoeffPowerSeries.constantCoeff.{u_1} {R : Type u_1} [Semiring R] : PowerSeries R →+* RThe constant coefficient of a formal power series.  h₂PowerSeries K) :
  h₁PowerSeries K =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. h₂PowerSeries K

theorem PowerSeries.invOnePlusX_subst_expbar_mul_exp.{u_1}
  {KType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [CommRingCommRing.{u} (α : Type u) : Type uA commutative ring is a ring with commutative multiplication.  KType u_1]
  [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 ℚRat : TypeRational numbers, implemented as a pair of integers `num / den` such that the
denominator is positive and the numerator and denominator are coprime.
 KType u_1] :
  PowerSeries.substPowerSeries.subst.{u_2, u_3, u_4} {R : Type u_2} [CommRing R] {τ : Type u_3} {S : Type u_4} [CommRing S] [Algebra R S]
  (a : MvPowerSeries τ S) (f : PowerSeries R) : MvPowerSeries τ SSubstitution of power series into a power series.  (PowerSeries.expbarPowerSeries.expbar.{u_1} (K : Type u_1) [CommRing K] [Algebra ℚ K] : PowerSeries KThe shifted exponential series `expbar = exp - 1 = ∑_{n≥1} 1/n! · x^n`.
This is `\overline{\exp}` in Definition 7.8.2 (def.fps.exp-log).  KType u_1)
        (PowerSeries.invOnePlusXPowerSeries.invOnePlusX.{u_1} (K : Type u_1) [CommRing K] [Algebra ℚ K] : PowerSeries KThe series `(1+x)⁻¹ = ∑_{n≥0} (-1)^n x^n`.  KType u_1) *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`.
      PowerSeries.expPowerSeries.exp.{u_1} (A : Type u_1) [Ring A] [Algebra ℚ A] : PowerSeries APower series for the exponential function at zero.  KType u_1 =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
    1

theorem PowerSeries.constantCoeff_subst_of_constantCoeff_zero.{u_1}
  {KType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [CommRingCommRing.{u} (α : Type u) : Type uA commutative ring is a ring with commutative multiplication.  KType u_1]
  {fPowerSeries K gPowerSeries K : PowerSeriesPowerSeries.{u_1} (R : Type u_1) : Type u_1Formal power series over a coefficient type `R`  KType u_1}
  (hgPowerSeries.constantCoeff g = 0 : PowerSeries.constantCoeffPowerSeries.constantCoeff.{u_1} {R : Type u_1} [Semiring R] : PowerSeries R →+* RThe constant coefficient of a formal power series.  gPowerSeries K =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. 0) :
  PowerSeries.constantCoeffPowerSeries.constantCoeff.{u_1} {R : Type u_1} [Semiring R] : PowerSeries R →+* RThe constant coefficient of a formal power series. 
      (PowerSeries.substPowerSeries.subst.{u_2, u_3, u_4} {R : Type u_2} [CommRing R] {τ : Type u_3} {S : Type u_4} [CommRing S] [Algebra R S]
  (a : MvPowerSeries τ S) (f : PowerSeries R) : MvPowerSeries τ SSubstitution of power series into a power series.  gPowerSeries K fPowerSeries K) =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
    PowerSeries.constantCoeffPowerSeries.constantCoeff.{u_1} {R : Type u_1} [Semiring R] : PowerSeries R →+* RThe constant coefficient of a formal power series.  fPowerSeries K

theorem PowerSeries.expbar_comp_logbar.{u_1}
  {KType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [CommRingCommRing.{u} (α : Type u) : Type uA commutative ring is a ring with commutative multiplication.  KType u_1]
  [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 ℚRat : TypeRational numbers, implemented as a pair of integers `num / den` such that the
denominator is positive and the numerator and denominator are coprime.
 KType u_1] :
  PowerSeries.substPowerSeries.subst.{u_2, u_3, u_4} {R : Type u_2} [CommRing R] {τ : Type u_3} {S : Type u_4} [CommRing S] [Algebra R S]
  (a : MvPowerSeries τ S) (f : PowerSeries R) : MvPowerSeries τ SSubstitution of power series into a power series.  (PowerSeries.logbarPowerSeries.logbar.{u_1} (K : Type u_1) [CommRing K] [Algebra ℚ K] : PowerSeries KThe logarithm series `logbar = ∑_{n≥1} (-1)^{n-1}/n · x^n`, which is the Mercator series
for `log(1+x)`. This is `\overline{\log}` in Definition 7.8.2 (def.fps.exp-log).  KType u_1)
      (PowerSeries.expbarPowerSeries.expbar.{u_1} (K : Type u_1) [CommRing K] [Algebra ℚ K] : PowerSeries KThe shifted exponential series `expbar = exp - 1 = ∑_{n≥1} 1/n! · x^n`.
This is `\overline{\exp}` in Definition 7.8.2 (def.fps.exp-log).  KType u_1) =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
    PowerSeries.XPowerSeries.X.{u_1} {R : Type u_1} [Semiring R] : PowerSeries RThe variable of the formal power series ring. 

theorem PowerSeries.logbar_comp_expbar.{u_1}
  {KType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [CommRingCommRing.{u} (α : Type u) : Type uA commutative ring is a ring with commutative multiplication.  KType u_1]
  [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 ℚRat : TypeRational numbers, implemented as a pair of integers `num / den` such that the
denominator is positive and the numerator and denominator are coprime.
 KType u_1] :
  PowerSeries.substPowerSeries.subst.{u_2, u_3, u_4} {R : Type u_2} [CommRing R] {τ : Type u_3} {S : Type u_4} [CommRing S] [Algebra R S]
  (a : MvPowerSeries τ S) (f : PowerSeries R) : MvPowerSeries τ SSubstitution of power series into a power series.  (PowerSeries.expbarPowerSeries.expbar.{u_1} (K : Type u_1) [CommRing K] [Algebra ℚ K] : PowerSeries KThe shifted exponential series `expbar = exp - 1 = ∑_{n≥1} 1/n! · x^n`.
This is `\overline{\exp}` in Definition 7.8.2 (def.fps.exp-log).  KType u_1)
      (PowerSeries.logbarPowerSeries.logbar.{u_1} (K : Type u_1) [CommRing K] [Algebra ℚ K] : PowerSeries KThe logarithm series `logbar = ∑_{n≥1} (-1)^{n-1}/n · x^n`, which is the Mercator series
for `log(1+x)`. This is `\overline{\log}` in Definition 7.8.2 (def.fps.exp-log).  KType u_1) =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
    PowerSeries.XPowerSeries.X.{u_1} {R : Type u_1} [Semiring R] : PowerSeries RThe variable of the formal power series ring. 

theorem PowerSeries.PowerSeries₀.subst_mem.{u_2}
  {KType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [CommRingCommRing.{u} (α : Type u) : Type uA commutative ring is a ring with commutative multiplication.  KType u_2]
  {fPowerSeries K gPowerSeries K : PowerSeriesPowerSeries.{u_1} (R : Type u_1) : Type u_1Formal power series over a coefficient type `R`  KType u_2}
  (hff ∈ PowerSeries.PowerSeries₀ : fPowerSeries K ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`. PowerSeries.PowerSeries₀PowerSeries.PowerSeries₀.{u_2} {R : Type u_2} [CommRing R] : Set (PowerSeries R)`R⟦X⟧₀` is the set of FPS with constant term 0.
This is Definition 7.8.6(a) (def.fps.Exp-Log-maps). )
  (hgg ∈ PowerSeries.PowerSeries₀ : gPowerSeries K ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`. PowerSeries.PowerSeries₀PowerSeries.PowerSeries₀.{u_2} {R : Type u_2} [CommRing R] : Set (PowerSeries R)`R⟦X⟧₀` is the set of FPS with constant term 0.
This is Definition 7.8.6(a) (def.fps.Exp-Log-maps). ) :
  PowerSeries.substPowerSeries.subst.{u_2, u_3, u_4} {R : Type u_2} [CommRing R] {τ : Type u_3} {S : Type u_4} [CommRing S] [Algebra R S]
  (a : MvPowerSeries τ S) (f : PowerSeries R) : MvPowerSeries τ SSubstitution of power series into a power series.  gPowerSeries K fPowerSeries K ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`.
    PowerSeries.PowerSeries₀PowerSeries.PowerSeries₀.{u_2} {R : Type u_2} [CommRing R] : Set (PowerSeries R)`R⟦X⟧₀` is the set of FPS with constant term 0.
This is Definition 7.8.6(a) (def.fps.Exp-Log-maps). 

theorem PowerSeries.PowerSeries₁.subst_mem.{u_2}
  {KType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [CommRingCommRing.{u} (α : Type u) : Type uA commutative ring is a ring with commutative multiplication.  KType u_2]
  {fPowerSeries K gPowerSeries K : PowerSeriesPowerSeries.{u_1} (R : Type u_1) : Type u_1Formal power series over a coefficient type `R`  KType u_2}
  (hff ∈ PowerSeries.PowerSeries₁ : fPowerSeries K ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`. PowerSeries.PowerSeries₁PowerSeries.PowerSeries₁.{u_2} {R : Type u_2} [CommRing R] : Set (PowerSeries R)`R⟦X⟧₁` is the set of FPS with constant term 1.
This is Definition 7.8.6(b) (def.fps.Exp-Log-maps). )
  (hgg ∈ PowerSeries.PowerSeries₀ : gPowerSeries K ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`. PowerSeries.PowerSeries₀PowerSeries.PowerSeries₀.{u_2} {R : Type u_2} [CommRing R] : Set (PowerSeries R)`R⟦X⟧₀` is the set of FPS with constant term 0.
This is Definition 7.8.6(a) (def.fps.Exp-Log-maps). ) :
  PowerSeries.substPowerSeries.subst.{u_2, u_3, u_4} {R : Type u_2} [CommRing R] {τ : Type u_3} {S : Type u_4} [CommRing S] [Algebra R S]
  (a : MvPowerSeries τ S) (f : PowerSeries R) : MvPowerSeries τ SSubstitution of power series into a power series.  gPowerSeries K fPowerSeries K ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`.
    PowerSeries.PowerSeries₁PowerSeries.PowerSeries₁.{u_2} {R : Type u_2} [CommRing R] : Set (PowerSeries R)`R⟦X⟧₁` is the set of FPS with constant term 1.
This is Definition 7.8.6(b) (def.fps.Exp-Log-maps). 

theorem PowerSeries.exp_subst_mem_PowerSeries₁.{u_2}
  {KType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [CommRingCommRing.{u} (α : Type u) : Type uA commutative ring is a ring with commutative multiplication.  KType u_2]
  [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 ℚRat : TypeRational numbers, implemented as a pair of integers `num / den` such that the
denominator is positive and the numerator and denominator are coprime.
 KType u_2] {gPowerSeries K : PowerSeriesPowerSeries.{u_1} (R : Type u_1) : Type u_1Formal power series over a coefficient type `R`  KType u_2}
  (hgg ∈ PowerSeries.PowerSeries₀ : gPowerSeries K ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`. PowerSeries.PowerSeries₀PowerSeries.PowerSeries₀.{u_2} {R : Type u_2} [CommRing R] : Set (PowerSeries R)`R⟦X⟧₀` is the set of FPS with constant term 0.
This is Definition 7.8.6(a) (def.fps.Exp-Log-maps). ) :
  PowerSeries.substPowerSeries.subst.{u_2, u_3, u_4} {R : Type u_2} [CommRing R] {τ : Type u_3} {S : Type u_4} [CommRing S] [Algebra R S]
  (a : MvPowerSeries τ S) (f : PowerSeries R) : MvPowerSeries τ SSubstitution of power series into a power series.  gPowerSeries K
      (PowerSeries.expPowerSeries.exp.{u_1} (A : Type u_1) [Ring A] [Algebra ℚ A] : PowerSeries APower series for the exponential function at zero.  KType u_2) ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`.
    PowerSeries.PowerSeries₁PowerSeries.PowerSeries₁.{u_2} {R : Type u_2} [CommRing R] : Set (PowerSeries R)`R⟦X⟧₁` is the set of FPS with constant term 1.
This is Definition 7.8.6(b) (def.fps.Exp-Log-maps). 

theorem PowerSeries.logbar_subst_sub_one_mem_PowerSeries₀.{u_2}
  {KType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [CommRingCommRing.{u} (α : Type u) : Type uA commutative ring is a ring with commutative multiplication.  KType u_2]
  [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 ℚRat : TypeRational numbers, implemented as a pair of integers `num / den` such that the
denominator is positive and the numerator and denominator are coprime.
 KType u_2] {fPowerSeries K : PowerSeriesPowerSeries.{u_1} (R : Type u_1) : Type u_1Formal power series over a coefficient type `R`  KType u_2}
  (hff ∈ PowerSeries.PowerSeries₁ : fPowerSeries K ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`. PowerSeries.PowerSeries₁PowerSeries.PowerSeries₁.{u_2} {R : Type u_2} [CommRing R] : Set (PowerSeries R)`R⟦X⟧₁` is the set of FPS with constant term 1.
This is Definition 7.8.6(b) (def.fps.Exp-Log-maps). ) :
  PowerSeries.substPowerSeries.subst.{u_2, u_3, u_4} {R : Type u_2} [CommRing R] {τ : Type u_3} {S : Type u_4} [CommRing S] [Algebra R S]
  (a : MvPowerSeries τ S) (f : PowerSeries R) : MvPowerSeries τ SSubstitution of power series into a power series.  (HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`.
The meaning of this notation is type-dependent.
* For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator).fPowerSeries K -HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`.
The meaning of this notation is type-dependent.
* For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator). 1)HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`.
The meaning of this notation is type-dependent.
* For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator).
      (PowerSeries.logbarPowerSeries.logbar.{u_1} (K : Type u_1) [CommRing K] [Algebra ℚ K] : PowerSeries KThe logarithm series `logbar = ∑_{n≥1} (-1)^{n-1}/n · x^n`, which is the Mercator series
for `log(1+x)`. This is `\overline{\log}` in Definition 7.8.2 (def.fps.exp-log).  KType u_2) ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`.
    PowerSeries.PowerSeries₀PowerSeries.PowerSeries₀.{u_2} {R : Type u_2} [CommRing R] : Set (PowerSeries R)`R⟦X⟧₀` is the set of FPS with constant term 0.
This is Definition 7.8.6(a) (def.fps.Exp-Log-maps). 

theorem PowerSeries.Log_Exp.{u_2} {KType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [CommRingCommRing.{u} (α : Type u) : Type uA commutative ring is a ring with commutative multiplication.  KType u_2] [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 ℚRat : TypeRational numbers, implemented as a pair of integers `num / den` such that the
denominator is positive and the numerator and denominator are coprime.
 KType u_2]
  (g↑PowerSeries.PowerSeries₀ : ↑PowerSeries.PowerSeries₀PowerSeries.PowerSeries₀.{u_2} {R : Type u_2} [CommRing R] : Set (PowerSeries R)`R⟦X⟧₀` is the set of FPS with constant term 0.
This is Definition 7.8.6(a) (def.fps.Exp-Log-maps). ) :
  PowerSeries.LogPowerSeries.Log.{u_2} {K : Type u_2} [CommRing K] [Algebra ℚ K] (f : ↑PowerSeries.PowerSeries₁) :
  ↑PowerSeries.PowerSeries₀The logarithm map `Log : K⟦X⟧₁ → K⟦X⟧₀` defined by `f ↦ logbar ∘ (f - 1)`.
This is Definition 7.8.6(c) (def.fps.Exp-Log-maps).  (PowerSeries.ExpPowerSeries.Exp.{u_2} {K : Type u_2} [CommRing K] [Algebra ℚ K] (g : ↑PowerSeries.PowerSeries₀) :
  ↑PowerSeries.PowerSeries₁The exponential map `Exp : K⟦X⟧₀ → K⟦X⟧₁` defined by `g ↦ exp ∘ g`.
This is Definition 7.8.6(c) (def.fps.Exp-Log-maps).  g↑PowerSeries.PowerSeries₀) =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. g↑PowerSeries.PowerSeries₀

theorem PowerSeries.Exp_Log.{u_2} {KType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [CommRingCommRing.{u} (α : Type u) : Type uA commutative ring is a ring with commutative multiplication.  KType u_2] [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 ℚRat : TypeRational numbers, implemented as a pair of integers `num / den` such that the
denominator is positive and the numerator and denominator are coprime.
 KType u_2]
  (f↑PowerSeries.PowerSeries₁ : ↑PowerSeries.PowerSeries₁PowerSeries.PowerSeries₁.{u_2} {R : Type u_2} [CommRing R] : Set (PowerSeries R)`R⟦X⟧₁` is the set of FPS with constant term 1.
This is Definition 7.8.6(b) (def.fps.Exp-Log-maps). ) :
  PowerSeries.ExpPowerSeries.Exp.{u_2} {K : Type u_2} [CommRing K] [Algebra ℚ K] (g : ↑PowerSeries.PowerSeries₀) :
  ↑PowerSeries.PowerSeries₁The exponential map `Exp : K⟦X⟧₀ → K⟦X⟧₁` defined by `g ↦ exp ∘ g`.
This is Definition 7.8.6(c) (def.fps.Exp-Log-maps).  (PowerSeries.LogPowerSeries.Log.{u_2} {K : Type u_2} [CommRing K] [Algebra ℚ K] (f : ↑PowerSeries.PowerSeries₁) :
  ↑PowerSeries.PowerSeries₀The logarithm map `Log : K⟦X⟧₁ → K⟦X⟧₀` defined by `f ↦ logbar ∘ (f - 1)`.
This is Definition 7.8.6(c) (def.fps.Exp-Log-maps).  f↑PowerSeries.PowerSeries₁) =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. f↑PowerSeries.PowerSeries₁

theorem PowerSeries.Exp_Log_inverse.{u_2}
  {KType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [CommRingCommRing.{u} (α : Type u) : Type uA commutative ring is a ring with commutative multiplication.  KType u_2]
  [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 ℚRat : TypeRational numbers, implemented as a pair of integers `num / den` such that the
denominator is positive and the numerator and denominator are coprime.
 KType u_2] :
  Function.LeftInverseFunction.LeftInverse.{u_1, u_2} {α : Sort u_1} {β : Sort u_2} (g : β → α) (f : α → β) : Prop`LeftInverse g f` means that `g` is a left inverse to `f`. That is, `g ∘ f = id`.  PowerSeries.LogPowerSeries.Log.{u_2} {K : Type u_2} [CommRing K] [Algebra ℚ K] (f : ↑PowerSeries.PowerSeries₁) :
  ↑PowerSeries.PowerSeries₀The logarithm map `Log : K⟦X⟧₁ → K⟦X⟧₀` defined by `f ↦ logbar ∘ (f - 1)`.
This is Definition 7.8.6(c) (def.fps.Exp-Log-maps). 
      PowerSeries.ExpPowerSeries.Exp.{u_2} {K : Type u_2} [CommRing K] [Algebra ℚ K] (g : ↑PowerSeries.PowerSeries₀) :
  ↑PowerSeries.PowerSeries₁The exponential map `Exp : K⟦X⟧₀ → K⟦X⟧₁` defined by `g ↦ exp ∘ g`.
This is Definition 7.8.6(c) (def.fps.Exp-Log-maps).  ∧And (a b : Prop) : Prop`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be
constructed and destructed like a pair: if `ha : a` and `hb : b` then
`⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.


Conventions for notations in identifiers:

 * The recommended spelling of `∧` in identifiers is `and`.

 * The recommended spelling of `/\` in identifiers is `and` (prefer `∧` over `/\`).
    Function.RightInverseFunction.RightInverse.{u_1, u_2} {α : Sort u_1} {β : Sort u_2} (g : β → α) (f : α → β) : Prop`RightInverse g f` means that `g` is a right inverse to `f`. That is, `f ∘ g = id`.  PowerSeries.LogPowerSeries.Log.{u_2} {K : Type u_2} [CommRing K] [Algebra ℚ K] (f : ↑PowerSeries.PowerSeries₁) :
  ↑PowerSeries.PowerSeries₀The logarithm map `Log : K⟦X⟧₁ → K⟦X⟧₀` defined by `f ↦ logbar ∘ (f - 1)`.
This is Definition 7.8.6(c) (def.fps.Exp-Log-maps). 
      PowerSeries.ExpPowerSeries.Exp.{u_2} {K : Type u_2} [CommRing K] [Algebra ℚ K] (g : ↑PowerSeries.PowerSeries₀) :
  ↑PowerSeries.PowerSeries₁The exponential map `Exp : K⟦X⟧₀ → K⟦X⟧₁` defined by `g ↦ exp ∘ g`.
This is Definition 7.8.6(c) (def.fps.Exp-Log-maps). 

theorem PowerSeries.sub_one_mem_PowerSeries₀.{u_2}
  {RType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [CommRingCommRing.{u} (α : Type u) : Type uA commutative ring is a ring with commutative multiplication.  RType u_2]
  {fPowerSeries R : PowerSeriesPowerSeries.{u_1} (R : Type u_1) : Type u_1Formal power series over a coefficient type `R`  RType u_2}
  (hff ∈ PowerSeries.PowerSeries₁ : fPowerSeries R ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`. PowerSeries.PowerSeries₁PowerSeries.PowerSeries₁.{u_2} {R : Type u_2} [CommRing R] : Set (PowerSeries R)`R⟦X⟧₁` is the set of FPS with constant term 1.
This is Definition 7.8.6(b) (def.fps.Exp-Log-maps). ) :
  fPowerSeries R -HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`.
The meaning of this notation is type-dependent.
* For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator). 1 ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`. PowerSeries.PowerSeries₀PowerSeries.PowerSeries₀.{u_2} {R : Type u_2} [CommRing R] : Set (PowerSeries R)`R⟦X⟧₀` is the set of FPS with constant term 0.
This is Definition 7.8.6(a) (def.fps.Exp-Log-maps). 

theorem PowerSeries.eq_of_derivative_eq_mul_self.{u_2}
  {KType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [CommRingCommRing.{u} (α : Type u) : Type uA commutative ring is a ring with commutative multiplication.  KType u_2]
  [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 ℚRat : TypeRational numbers, implemented as a pair of integers `num / den` such that the
denominator is positive and the numerator and denominator are coprime.
 KType u_2] {h₁PowerSeries K h₂PowerSeries K gPowerSeries K : PowerSeriesPowerSeries.{u_1} (R : Type u_1) : Type u_1Formal power series over a coefficient type `R`  KType u_2}
  (hd₁(PowerSeries.derivative K) h₁ = h₁ * g :
    (PowerSeries.derivativePowerSeries.derivative.{u_1} (R : Type u_1) [CommSemiring R] : Derivation R (PowerSeries R) (PowerSeries R)The formal derivative of a formal power series  KType u_2) h₁PowerSeries K =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
      h₁PowerSeries K *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`. gPowerSeries K)
  (hd₂(PowerSeries.derivative K) h₂ = h₂ * g :
    (PowerSeries.derivativePowerSeries.derivative.{u_1} (R : Type u_1) [CommSemiring R] : Derivation R (PowerSeries R) (PowerSeries R)The formal derivative of a formal power series  KType u_2) h₂PowerSeries K =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
      h₂PowerSeries K *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`. gPowerSeries K)
  (hcPowerSeries.constantCoeff h₁ = PowerSeries.constantCoeff h₂ :
    PowerSeries.constantCoeffPowerSeries.constantCoeff.{u_1} {R : Type u_1} [Semiring R] : PowerSeries R →+* RThe constant coefficient of a formal power series.  h₁PowerSeries K =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
      PowerSeries.constantCoeffPowerSeries.constantCoeff.{u_1} {R : Type u_1} [Semiring R] : PowerSeries R →+* RThe constant coefficient of a formal power series.  h₂PowerSeries K) :
  h₁PowerSeries K =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. h₂PowerSeries K