theorem AlgebraicCombinatorics.FPS.hasConstantTermOne_mul.{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}
  (hfAlgebraicCombinatorics.FPS.HasConstantTermOne f :
    AlgebraicCombinatorics.FPS.HasConstantTermOneAlgebraicCombinatorics.FPS.HasConstantTermOne.{u_1} {K : Type u_1} [CommRing K] (f : PowerSeries K) : PropAn FPS has constant term 1.
This is the condition for f ∈ K⟦X⟧₁ in the source.
Label: def.fps.Exp-Log-maps (b)

Note: This is definitionally equivalent to membership in `PowerSeries₁` from ExpLog.lean:
`HasConstantTermOne f ↔ f ∈ PowerSeries₁`. The `Prop` form is used here for convenience
in hypotheses, while `PowerSeries₁` (a `Set`) is used in ExpLog.lean for subgroup structures. 
      fPowerSeries K)
  (hgAlgebraicCombinatorics.FPS.HasConstantTermOne g :
    AlgebraicCombinatorics.FPS.HasConstantTermOneAlgebraicCombinatorics.FPS.HasConstantTermOne.{u_1} {K : Type u_1} [CommRing K] (f : PowerSeries K) : PropAn FPS has constant term 1.
This is the condition for f ∈ K⟦X⟧₁ in the source.
Label: def.fps.Exp-Log-maps (b)

Note: This is definitionally equivalent to membership in `PowerSeries₁` from ExpLog.lean:
`HasConstantTermOne f ↔ f ∈ PowerSeries₁`. The `Prop` form is used here for convenience
in hypotheses, while `PowerSeries₁` (a `Set`) is used in ExpLog.lean for subgroup structures. 
      gPowerSeries K) :
  AlgebraicCombinatorics.FPS.HasConstantTermOneAlgebraicCombinatorics.FPS.HasConstantTermOne.{u_1} {K : Type u_1} [CommRing K] (f : PowerSeries K) : PropAn FPS has constant term 1.
This is the condition for f ∈ K⟦X⟧₁ in the source.
Label: def.fps.Exp-Log-maps (b)

Note: This is definitionally equivalent to membership in `PowerSeries₁` from ExpLog.lean:
`HasConstantTermOne f ↔ f ∈ PowerSeries₁`. The `Prop` form is used here for convenience
in hypotheses, while `PowerSeries₁` (a `Set`) is used in ExpLog.lean for subgroup structures. 
    (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`.fPowerSeries 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)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`.

theorem AlgebraicCombinatorics.FPS.hasConstantTermOne_one_add_X.{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] :
  AlgebraicCombinatorics.FPS.HasConstantTermOneAlgebraicCombinatorics.FPS.HasConstantTermOne.{u_1} {K : Type u_1} [CommRing K] (f : PowerSeries K) : PropAn FPS has constant term 1.
This is the condition for f ∈ K⟦X⟧₁ in the source.
Label: def.fps.Exp-Log-maps (b)

Note: This is definitionally equivalent to membership in `PowerSeries₁` from ExpLog.lean:
`HasConstantTermOne f ↔ f ∈ PowerSeries₁`. The `Prop` form is used here for convenience
in hypotheses, while `PowerSeries₁` (a `Set`) is used in ExpLog.lean for subgroup structures. 
    (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`. PowerSeries.XPowerSeries.X.{u_1} {R : Type u_1} [Semiring R] : PowerSeries RThe variable of the formal power series ring. )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`.

theorem AlgebraicCombinatorics.FPS.constantCoeff_logSeries.{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.constantCoeffPowerSeries.constantCoeff.{u_1} {R : Type u_1} [Semiring R] : PowerSeries R →+* RThe constant coefficient of a formal power series. 
      AlgebraicCombinatorics.FPS.logSeriesAlgebraicCombinatorics.FPS.logSeries.{u_1} {K : Type u_1} [CommRing K] [Algebra ℚ K] : PowerSeries KThe logarithm series: log(1+x) = x - x²/2 + x³/3 - x⁴/4 + ...
This is `\overline{log}` in the source notation.
Label: def.fps.logbar  =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

theorem AlgebraicCombinatorics.FPS.fpsLog_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] :
  AlgebraicCombinatorics.FPS.fpsLogAlgebraicCombinatorics.FPS.fpsLog.{u_1} {K : Type u_1} [CommRing K] [Algebra ℚ K] (f : PowerSeries K) : PowerSeries KThe Log map: Log(f) = log_series(f-1) = logSeries.subst (f-1)
This is well-defined when f has constant term 1.
Label: def.fps.Exp-Log-maps  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`. 0

theorem AlgebraicCombinatorics.FPS.constantCoeff_fpsLog.{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] {fPowerSeries K : PowerSeriesPowerSeries.{u_1} (R : Type u_1) : Type u_1Formal power series over a coefficient type `R`  KType u_1}
  (hfAlgebraicCombinatorics.FPS.HasConstantTermOne f :
    AlgebraicCombinatorics.FPS.HasConstantTermOneAlgebraicCombinatorics.FPS.HasConstantTermOne.{u_1} {K : Type u_1} [CommRing K] (f : PowerSeries K) : PropAn FPS has constant term 1.
This is the condition for f ∈ K⟦X⟧₁ in the source.
Label: def.fps.Exp-Log-maps (b)

Note: This is definitionally equivalent to membership in `PowerSeries₁` from ExpLog.lean:
`HasConstantTermOne f ↔ f ∈ PowerSeries₁`. The `Prop` form is used here for convenience
in hypotheses, while `PowerSeries₁` (a `Set`) is used in ExpLog.lean for subgroup structures. 
      fPowerSeries K) :
  PowerSeries.constantCoeffPowerSeries.constantCoeff.{u_1} {R : Type u_1} [Semiring R] : PowerSeries R →+* RThe constant coefficient of a formal power series. 
      (AlgebraicCombinatorics.FPS.fpsLogAlgebraicCombinatorics.FPS.fpsLog.{u_1} {K : Type u_1} [CommRing K] [Algebra ℚ K] (f : PowerSeries K) : PowerSeries KThe Log map: Log(f) = log_series(f-1) = logSeries.subst (f-1)
This is well-defined when f has constant term 1.
Label: def.fps.Exp-Log-maps 
        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`.
    0

theorem AlgebraicCombinatorics.FPS.fpsLog_mul.{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] {fPowerSeries K gPowerSeries K : PowerSeriesPowerSeries.{u_1} (R : Type u_1) : Type u_1Formal power series over a coefficient type `R`  KType u_1}
  (hfAlgebraicCombinatorics.FPS.HasConstantTermOne f :
    AlgebraicCombinatorics.FPS.HasConstantTermOneAlgebraicCombinatorics.FPS.HasConstantTermOne.{u_1} {K : Type u_1} [CommRing K] (f : PowerSeries K) : PropAn FPS has constant term 1.
This is the condition for f ∈ K⟦X⟧₁ in the source.
Label: def.fps.Exp-Log-maps (b)

Note: This is definitionally equivalent to membership in `PowerSeries₁` from ExpLog.lean:
`HasConstantTermOne f ↔ f ∈ PowerSeries₁`. The `Prop` form is used here for convenience
in hypotheses, while `PowerSeries₁` (a `Set`) is used in ExpLog.lean for subgroup structures. 
      fPowerSeries K)
  (hgAlgebraicCombinatorics.FPS.HasConstantTermOne g :
    AlgebraicCombinatorics.FPS.HasConstantTermOneAlgebraicCombinatorics.FPS.HasConstantTermOne.{u_1} {K : Type u_1} [CommRing K] (f : PowerSeries K) : PropAn FPS has constant term 1.
This is the condition for f ∈ K⟦X⟧₁ in the source.
Label: def.fps.Exp-Log-maps (b)

Note: This is definitionally equivalent to membership in `PowerSeries₁` from ExpLog.lean:
`HasConstantTermOne f ↔ f ∈ PowerSeries₁`. The `Prop` form is used here for convenience
in hypotheses, while `PowerSeries₁` (a `Set`) is used in ExpLog.lean for subgroup structures. 
      gPowerSeries K) :
  AlgebraicCombinatorics.FPS.fpsLogAlgebraicCombinatorics.FPS.fpsLog.{u_1} {K : Type u_1} [CommRing K] [Algebra ℚ K] (f : PowerSeries K) : PowerSeries KThe Log map: Log(f) = log_series(f-1) = logSeries.subst (f-1)
This is well-defined when f has constant term 1.
Label: def.fps.Exp-Log-maps 
      (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`.fPowerSeries 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)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`. =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`.
    AlgebraicCombinatorics.FPS.fpsLogAlgebraicCombinatorics.FPS.fpsLog.{u_1} {K : Type u_1} [CommRing K] [Algebra ℚ K] (f : PowerSeries K) : PowerSeries KThe Log map: Log(f) = log_series(f-1) = logSeries.subst (f-1)
This is well-defined when f has constant term 1.
Label: def.fps.Exp-Log-maps  fPowerSeries 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`.
      AlgebraicCombinatorics.FPS.fpsLogAlgebraicCombinatorics.FPS.fpsLog.{u_1} {K : Type u_1} [CommRing K] [Algebra ℚ K] (f : PowerSeries K) : PowerSeries KThe Log map: Log(f) = log_series(f-1) = logSeries.subst (f-1)
This is well-defined when f has constant term 1.
Label: def.fps.Exp-Log-maps  gPowerSeries K

theorem AlgebraicCombinatorics.FPS.fpsExp_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]
  [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] :
  AlgebraicCombinatorics.FPS.fpsExpAlgebraicCombinatorics.FPS.fpsExp.{u_1} {K : Type u_1} [CommRing K] [Algebra ℚ K] (g : PowerSeries K) : PowerSeries KThe Exp map: Exp(g) = exp(g) = (exp K).subst g
This is well-defined when g has constant term 0.
Label: def.fps.Exp-Log-maps  0 =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 AlgebraicCombinatorics.FPS.hasConstantTermOne_fpsExp.{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) :
  AlgebraicCombinatorics.FPS.HasConstantTermOneAlgebraicCombinatorics.FPS.HasConstantTermOne.{u_1} {K : Type u_1} [CommRing K] (f : PowerSeries K) : PropAn FPS has constant term 1.
This is the condition for f ∈ K⟦X⟧₁ in the source.
Label: def.fps.Exp-Log-maps (b)

Note: This is definitionally equivalent to membership in `PowerSeries₁` from ExpLog.lean:
`HasConstantTermOne f ↔ f ∈ PowerSeries₁`. The `Prop` form is used here for convenience
in hypotheses, while `PowerSeries₁` (a `Set`) is used in ExpLog.lean for subgroup structures. 
    (AlgebraicCombinatorics.FPS.fpsExpAlgebraicCombinatorics.FPS.fpsExp.{u_1} {K : Type u_1} [CommRing K] [Algebra ℚ K] (g : PowerSeries K) : PowerSeries KThe Exp map: Exp(g) = exp(g) = (exp K).subst g
This is well-defined when g has constant term 0.
Label: def.fps.Exp-Log-maps  gPowerSeries K)

theorem AlgebraicCombinatorics.FPS.fpsExp_add.{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] {xPowerSeries K yPowerSeries K : PowerSeriesPowerSeries.{u_1} (R : Type u_1) : Type u_1Formal power series over a coefficient type `R`  KType u_1}
  (hxPowerSeries.constantCoeff x = 0 : PowerSeries.constantCoeffPowerSeries.constantCoeff.{u_1} {R : Type u_1} [Semiring R] : PowerSeries R →+* RThe constant coefficient of a formal power series.  xPowerSeries 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)
  (hyPowerSeries.constantCoeff y = 0 : PowerSeries.constantCoeffPowerSeries.constantCoeff.{u_1} {R : Type u_1} [Semiring R] : PowerSeries R →+* RThe constant coefficient of a formal power series.  yPowerSeries 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) :
  AlgebraicCombinatorics.FPS.fpsExpAlgebraicCombinatorics.FPS.fpsExp.{u_1} {K : Type u_1} [CommRing K] [Algebra ℚ K] (g : PowerSeries K) : PowerSeries KThe Exp map: Exp(g) = exp(g) = (exp K).subst g
This is well-defined when g has constant term 0.
Label: def.fps.Exp-Log-maps 
      (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`.xPowerSeries 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`. yPowerSeries 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`. =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`.
    AlgebraicCombinatorics.FPS.fpsExpAlgebraicCombinatorics.FPS.fpsExp.{u_1} {K : Type u_1} [CommRing K] [Algebra ℚ K] (g : PowerSeries K) : PowerSeries KThe Exp map: Exp(g) = exp(g) = (exp K).subst g
This is well-defined when g has constant term 0.
Label: def.fps.Exp-Log-maps  xPowerSeries 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`.
      AlgebraicCombinatorics.FPS.fpsExpAlgebraicCombinatorics.FPS.fpsExp.{u_1} {K : Type u_1} [CommRing K] [Algebra ℚ K] (g : PowerSeries K) : PowerSeries KThe Exp map: Exp(g) = exp(g) = (exp K).subst g
This is well-defined when g has constant term 0.
Label: def.fps.Exp-Log-maps  yPowerSeries K

theorem AlgebraicCombinatorics.FPS.fpsPow_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]
  [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] (fPowerSeries K : PowerSeriesPowerSeries.{u_1} (R : Type u_1) : Type u_1Formal power series over a coefficient type `R`  KType u_1) :
  AlgebraicCombinatorics.FPS.fpsPowAlgebraicCombinatorics.FPS.fpsPow.{u_1} {K : Type u_1} [CommRing K] [Algebra ℚ K] (f : PowerSeries K) (c : K) :
  PowerSeries KThe c-th power of an FPS f with constant term 1.
f^c := Exp(c * Log(f)) = exp.subst (c * log_series.subst (f-1))
Label: def.fps.power-c  fPowerSeries K 0 =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 AlgebraicCombinatorics.FPS.hasConstantTermOne_fpsPow.{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] {fPowerSeries K : PowerSeriesPowerSeries.{u_1} (R : Type u_1) : Type u_1Formal power series over a coefficient type `R`  KType u_1}
  (hfAlgebraicCombinatorics.FPS.HasConstantTermOne f :
    AlgebraicCombinatorics.FPS.HasConstantTermOneAlgebraicCombinatorics.FPS.HasConstantTermOne.{u_1} {K : Type u_1} [CommRing K] (f : PowerSeries K) : PropAn FPS has constant term 1.
This is the condition for f ∈ K⟦X⟧₁ in the source.
Label: def.fps.Exp-Log-maps (b)

Note: This is definitionally equivalent to membership in `PowerSeries₁` from ExpLog.lean:
`HasConstantTermOne f ↔ f ∈ PowerSeries₁`. The `Prop` form is used here for convenience
in hypotheses, while `PowerSeries₁` (a `Set`) is used in ExpLog.lean for subgroup structures. 
      fPowerSeries K)
  (cK : KType u_1) :
  AlgebraicCombinatorics.FPS.HasConstantTermOneAlgebraicCombinatorics.FPS.HasConstantTermOne.{u_1} {K : Type u_1} [CommRing K] (f : PowerSeries K) : PropAn FPS has constant term 1.
This is the condition for f ∈ K⟦X⟧₁ in the source.
Label: def.fps.Exp-Log-maps (b)

Note: This is definitionally equivalent to membership in `PowerSeries₁` from ExpLog.lean:
`HasConstantTermOne f ↔ f ∈ PowerSeries₁`. The `Prop` form is used here for convenience
in hypotheses, while `PowerSeries₁` (a `Set`) is used in ExpLog.lean for subgroup structures. 
    (AlgebraicCombinatorics.FPS.fpsPowAlgebraicCombinatorics.FPS.fpsPow.{u_1} {K : Type u_1} [CommRing K] [Algebra ℚ K] (f : PowerSeries K) (c : K) :
  PowerSeries KThe c-th power of an FPS f with constant term 1.
f^c := Exp(c * Log(f)) = exp.subst (c * log_series.subst (f-1))
Label: def.fps.power-c  fPowerSeries K
      cK)

theorem AlgebraicCombinatorics.FPS.fpsPow_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] {fPowerSeries K : PowerSeriesPowerSeries.{u_1} (R : Type u_1) : Type u_1Formal power series over a coefficient type `R`  KType u_1}
  (hfAlgebraicCombinatorics.FPS.HasConstantTermOne f :
    AlgebraicCombinatorics.FPS.HasConstantTermOneAlgebraicCombinatorics.FPS.HasConstantTermOne.{u_1} {K : Type u_1} [CommRing K] (f : PowerSeries K) : PropAn FPS has constant term 1.
This is the condition for f ∈ K⟦X⟧₁ in the source.
Label: def.fps.Exp-Log-maps (b)

Note: This is definitionally equivalent to membership in `PowerSeries₁` from ExpLog.lean:
`HasConstantTermOne f ↔ f ∈ PowerSeries₁`. The `Prop` form is used here for convenience
in hypotheses, while `PowerSeries₁` (a `Set`) is used in ExpLog.lean for subgroup structures. 
      fPowerSeries K) :
  AlgebraicCombinatorics.FPS.fpsPowAlgebraicCombinatorics.FPS.fpsPow.{u_1} {K : Type u_1} [CommRing K] [Algebra ℚ K] (f : PowerSeries K) (c : K) :
  PowerSeries KThe c-th power of an FPS f with constant term 1.
f^c := Exp(c * Log(f)) = exp.subst (c * log_series.subst (f-1))
Label: def.fps.power-c  fPowerSeries K 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`.
    fPowerSeries K

theorem AlgebraicCombinatorics.FPS.fpsPow_add.{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] {fPowerSeries K : PowerSeriesPowerSeries.{u_1} (R : Type u_1) : Type u_1Formal power series over a coefficient type `R`  KType u_1}
  (hfAlgebraicCombinatorics.FPS.HasConstantTermOne f :
    AlgebraicCombinatorics.FPS.HasConstantTermOneAlgebraicCombinatorics.FPS.HasConstantTermOne.{u_1} {K : Type u_1} [CommRing K] (f : PowerSeries K) : PropAn FPS has constant term 1.
This is the condition for f ∈ K⟦X⟧₁ in the source.
Label: def.fps.Exp-Log-maps (b)

Note: This is definitionally equivalent to membership in `PowerSeries₁` from ExpLog.lean:
`HasConstantTermOne f ↔ f ∈ PowerSeries₁`. The `Prop` form is used here for convenience
in hypotheses, while `PowerSeries₁` (a `Set`) is used in ExpLog.lean for subgroup structures. 
      fPowerSeries K)
  (aK bK : KType u_1) :
  AlgebraicCombinatorics.FPS.fpsPowAlgebraicCombinatorics.FPS.fpsPow.{u_1} {K : Type u_1} [CommRing K] [Algebra ℚ K] (f : PowerSeries K) (c : K) :
  PowerSeries KThe c-th power of an FPS f with constant term 1.
f^c := Exp(c * Log(f)) = exp.subst (c * log_series.subst (f-1))
Label: def.fps.power-c  fPowerSeries 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`.aK +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`. bK)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`. =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`.
    AlgebraicCombinatorics.FPS.fpsPowAlgebraicCombinatorics.FPS.fpsPow.{u_1} {K : Type u_1} [CommRing K] [Algebra ℚ K] (f : PowerSeries K) (c : K) :
  PowerSeries KThe c-th power of an FPS f with constant term 1.
f^c := Exp(c * Log(f)) = exp.subst (c * log_series.subst (f-1))
Label: def.fps.power-c  fPowerSeries K
        aK *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`.
      AlgebraicCombinatorics.FPS.fpsPowAlgebraicCombinatorics.FPS.fpsPow.{u_1} {K : Type u_1} [CommRing K] [Algebra ℚ K] (f : PowerSeries K) (c : K) :
  PowerSeries KThe c-th power of an FPS f with constant term 1.
f^c := Exp(c * Log(f)) = exp.subst (c * log_series.subst (f-1))
Label: def.fps.power-c  fPowerSeries K
        bK

theorem AlgebraicCombinatorics.FPS.fpsPow_mul.{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] {fPowerSeries K gPowerSeries K : PowerSeriesPowerSeries.{u_1} (R : Type u_1) : Type u_1Formal power series over a coefficient type `R`  KType u_1}
  (hfAlgebraicCombinatorics.FPS.HasConstantTermOne f :
    AlgebraicCombinatorics.FPS.HasConstantTermOneAlgebraicCombinatorics.FPS.HasConstantTermOne.{u_1} {K : Type u_1} [CommRing K] (f : PowerSeries K) : PropAn FPS has constant term 1.
This is the condition for f ∈ K⟦X⟧₁ in the source.
Label: def.fps.Exp-Log-maps (b)

Note: This is definitionally equivalent to membership in `PowerSeries₁` from ExpLog.lean:
`HasConstantTermOne f ↔ f ∈ PowerSeries₁`. The `Prop` form is used here for convenience
in hypotheses, while `PowerSeries₁` (a `Set`) is used in ExpLog.lean for subgroup structures. 
      fPowerSeries K)
  (hgAlgebraicCombinatorics.FPS.HasConstantTermOne g :
    AlgebraicCombinatorics.FPS.HasConstantTermOneAlgebraicCombinatorics.FPS.HasConstantTermOne.{u_1} {K : Type u_1} [CommRing K] (f : PowerSeries K) : PropAn FPS has constant term 1.
This is the condition for f ∈ K⟦X⟧₁ in the source.
Label: def.fps.Exp-Log-maps (b)

Note: This is definitionally equivalent to membership in `PowerSeries₁` from ExpLog.lean:
`HasConstantTermOne f ↔ f ∈ PowerSeries₁`. The `Prop` form is used here for convenience
in hypotheses, while `PowerSeries₁` (a `Set`) is used in ExpLog.lean for subgroup structures. 
      gPowerSeries K)
  (aK : KType u_1) :
  AlgebraicCombinatorics.FPS.fpsPowAlgebraicCombinatorics.FPS.fpsPow.{u_1} {K : Type u_1} [CommRing K] [Algebra ℚ K] (f : PowerSeries K) (c : K) :
  PowerSeries KThe c-th power of an FPS f with constant term 1.
f^c := Exp(c * Log(f)) = exp.subst (c * log_series.subst (f-1))
Label: def.fps.power-c 
      (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`.fPowerSeries 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)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`. aK =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`.
    AlgebraicCombinatorics.FPS.fpsPowAlgebraicCombinatorics.FPS.fpsPow.{u_1} {K : Type u_1} [CommRing K] [Algebra ℚ K] (f : PowerSeries K) (c : K) :
  PowerSeries KThe c-th power of an FPS f with constant term 1.
f^c := Exp(c * Log(f)) = exp.subst (c * log_series.subst (f-1))
Label: def.fps.power-c  fPowerSeries K
        aK *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`.
      AlgebraicCombinatorics.FPS.fpsPowAlgebraicCombinatorics.FPS.fpsPow.{u_1} {K : Type u_1} [CommRing K] [Algebra ℚ K] (f : PowerSeries K) (c : K) :
  PowerSeries KThe c-th power of an FPS f with constant term 1.
f^c := Exp(c * Log(f)) = exp.subst (c * log_series.subst (f-1))
Label: def.fps.power-c  gPowerSeries K
        aK

theorem AlgebraicCombinatorics.FPS.fpsPow_pow.{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] {fPowerSeries K : PowerSeriesPowerSeries.{u_1} (R : Type u_1) : Type u_1Formal power series over a coefficient type `R`  KType u_1}
  (hfAlgebraicCombinatorics.FPS.HasConstantTermOne f :
    AlgebraicCombinatorics.FPS.HasConstantTermOneAlgebraicCombinatorics.FPS.HasConstantTermOne.{u_1} {K : Type u_1} [CommRing K] (f : PowerSeries K) : PropAn FPS has constant term 1.
This is the condition for f ∈ K⟦X⟧₁ in the source.
Label: def.fps.Exp-Log-maps (b)

Note: This is definitionally equivalent to membership in `PowerSeries₁` from ExpLog.lean:
`HasConstantTermOne f ↔ f ∈ PowerSeries₁`. The `Prop` form is used here for convenience
in hypotheses, while `PowerSeries₁` (a `Set`) is used in ExpLog.lean for subgroup structures. 
      fPowerSeries K)
  (aK bK : KType u_1) :
  AlgebraicCombinatorics.FPS.fpsPowAlgebraicCombinatorics.FPS.fpsPow.{u_1} {K : Type u_1} [CommRing K] [Algebra ℚ K] (f : PowerSeries K) (c : K) :
  PowerSeries KThe c-th power of an FPS f with constant term 1.
f^c := Exp(c * Log(f)) = exp.subst (c * log_series.subst (f-1))
Label: def.fps.power-c 
      (AlgebraicCombinatorics.FPS.fpsPowAlgebraicCombinatorics.FPS.fpsPow.{u_1} {K : Type u_1} [CommRing K] [Algebra ℚ K] (f : PowerSeries K) (c : K) :
  PowerSeries KThe c-th power of an FPS f with constant term 1.
f^c := Exp(c * Log(f)) = exp.subst (c * log_series.subst (f-1))
Label: def.fps.power-c  fPowerSeries K
        aK)
      bK =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`.
    AlgebraicCombinatorics.FPS.fpsPowAlgebraicCombinatorics.FPS.fpsPow.{u_1} {K : Type u_1} [CommRing K] [Algebra ℚ K] (f : PowerSeries K) (c : K) :
  PowerSeries KThe c-th power of an FPS f with constant term 1.
f^c := Exp(c * Log(f)) = exp.subst (c * log_series.subst (f-1))
Label: def.fps.power-c  fPowerSeries 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`.aK *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`. bK)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`.

theorem AlgebraicCombinatorics.FPS.fpsPow_nat.{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] [CharZeroCharZero.{u_1} (R : Type u_1) [AddMonoidWithOne R] : PropTypeclass for monoids with characteristic zero.
  (This is usually stated on fields but it makes sense for any additive monoid with 1.)

*Warning*: for a semiring `R`, `CharZero R` and `CharP R 0` need not coincide.
* `CharZero R` requires an injection `ℕ ↪ R`;
* `CharP R 0` asks that only `0 : ℕ` maps to `0 : R` under the map `ℕ → R`.
  For instance, endowing `{0, 1}` with addition given by `max` (i.e. `1` is absorbing), shows that
  `CharZero {0, 1}` does not hold and yet `CharP {0, 1} 0` does.
  This example is formalized in `Counterexamples/CharPZeroNeCharZero.lean`.
 KType u_1]
  {fPowerSeries K : PowerSeriesPowerSeries.{u_1} (R : Type u_1) : Type u_1Formal power series over a coefficient type `R`  KType u_1}
  (hfAlgebraicCombinatorics.FPS.HasConstantTermOne f :
    AlgebraicCombinatorics.FPS.HasConstantTermOneAlgebraicCombinatorics.FPS.HasConstantTermOne.{u_1} {K : Type u_1} [CommRing K] (f : PowerSeries K) : PropAn FPS has constant term 1.
This is the condition for f ∈ K⟦X⟧₁ in the source.
Label: def.fps.Exp-Log-maps (b)

Note: This is definitionally equivalent to membership in `PowerSeries₁` from ExpLog.lean:
`HasConstantTermOne f ↔ f ∈ PowerSeries₁`. The `Prop` form is used here for convenience
in hypotheses, while `PowerSeries₁` (a `Set`) is used in ExpLog.lean for subgroup structures. 
      fPowerSeries K)
  (nℕ : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
) :
  AlgebraicCombinatorics.FPS.fpsPowAlgebraicCombinatorics.FPS.fpsPow.{u_1} {K : Type u_1} [CommRing K] [Algebra ℚ K] (f : PowerSeries K) (c : K) :
  PowerSeries KThe c-th power of an FPS f with constant term 1.
f^c := Exp(c * Log(f)) = exp.subst (c * log_series.subst (f-1))
Label: def.fps.power-c  fPowerSeries K ↑nℕ =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`.
    fPowerSeries K ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ`a ^ b` computes `a` to the power of `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `^` in identifiers is `pow`. nℕ

theorem AlgebraicCombinatorics.FPS.generalizedNewtonBinomial.{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] [BinomialRingBinomialRing.{u_1} (R : Type u_1) [AddCommMonoid R] [Pow R ℕ] : Type u_1A binomial ring is a ring for which ascending Pochhammer evaluations are uniquely divisible by
suitable factorials. We define this notion as a mixin for additive commutative monoids with natural
number powers, but retain the ring name. We introduce `Ring.multichoose` as the uniquely defined
quotient.  KType u_1]
  [CharZeroCharZero.{u_1} (R : Type u_1) [AddMonoidWithOne R] : PropTypeclass for monoids with characteristic zero.
  (This is usually stated on fields but it makes sense for any additive monoid with 1.)

*Warning*: for a semiring `R`, `CharZero R` and `CharP R 0` need not coincide.
* `CharZero R` requires an injection `ℕ ↪ R`;
* `CharP R 0` asks that only `0 : ℕ` maps to `0 : R` under the map `ℕ → R`.
  For instance, endowing `{0, 1}` with addition given by `max` (i.e. `1` is absorbing), shows that
  `CharZero {0, 1}` does not hold and yet `CharP {0, 1} 0` does.
  This example is formalized in `Counterexamples/CharPZeroNeCharZero.lean`.
 KType u_1] (cK : KType u_1) :
  AlgebraicCombinatorics.FPS.fpsPowAlgebraicCombinatorics.FPS.fpsPow.{u_1} {K : Type u_1} [CommRing K] [Algebra ℚ K] (f : PowerSeries K) (c : K) :
  PowerSeries KThe c-th power of an FPS f with constant term 1.
f^c := Exp(c * Log(f)) = exp.subst (c * log_series.subst (f-1))
Label: def.fps.power-c 
      (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`. PowerSeries.XPowerSeries.X.{u_1} {R : Type u_1} [Semiring R] : PowerSeries RThe variable of the formal power series ring. )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`. cK =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.binomialSeriesPowerSeries.binomialSeries.{u_1, u_3} {R : Type u_1} [CommRing R] [BinomialRing R] (A : Type u_3) [One A] [SMul R A]
  (r : R) : PowerSeries AThe power series for `(1 + X) ^ r`.  KType u_1 cK

theorem AlgebraicCombinatorics.FPS.coeff_one_add_X_fpsPow.{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] [BinomialRingBinomialRing.{u_1} (R : Type u_1) [AddCommMonoid R] [Pow R ℕ] : Type u_1A binomial ring is a ring for which ascending Pochhammer evaluations are uniquely divisible by
suitable factorials. We define this notion as a mixin for additive commutative monoids with natural
number powers, but retain the ring name. We introduce `Ring.multichoose` as the uniquely defined
quotient.  KType u_1]
  [CharZeroCharZero.{u_1} (R : Type u_1) [AddMonoidWithOne R] : PropTypeclass for monoids with characteristic zero.
  (This is usually stated on fields but it makes sense for any additive monoid with 1.)

*Warning*: for a semiring `R`, `CharZero R` and `CharP R 0` need not coincide.
* `CharZero R` requires an injection `ℕ ↪ R`;
* `CharP R 0` asks that only `0 : ℕ` maps to `0 : R` under the map `ℕ → R`.
  For instance, endowing `{0, 1}` with addition given by `max` (i.e. `1` is absorbing), shows that
  `CharZero {0, 1}` does not hold and yet `CharP {0, 1} 0` does.
  This example is formalized in `Counterexamples/CharPZeroNeCharZero.lean`.
 KType u_1] (cK : KType u_1) (kℕ : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
) :
  (PowerSeries.coeffPowerSeries.coeff.{u_1} {R : Type u_1} [Semiring R] (n : ℕ) : PowerSeries R →ₗ[R] RThe `n`th coefficient of a formal power series.  kℕ)
      (AlgebraicCombinatorics.FPS.fpsPowAlgebraicCombinatorics.FPS.fpsPow.{u_1} {K : Type u_1} [CommRing K] [Algebra ℚ K] (f : PowerSeries K) (c : K) :
  PowerSeries KThe c-th power of an FPS f with constant term 1.
f^c := Exp(c * Log(f)) = exp.subst (c * log_series.subst (f-1))
Label: def.fps.power-c 
        (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`. PowerSeries.XPowerSeries.X.{u_1} {R : Type u_1} [Semiring R] : PowerSeries RThe variable of the formal power series ring. )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`. cK) =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`.
    Ring.chooseRing.choose.{u_1} {R : Type u_1} [AddCommGroupWithOne R] [Pow R ℕ] [BinomialRing R] (r : R) (n : ℕ) : RThe binomial coefficient `choose r n` generalizes the natural number `Nat.choose` function,
interpreted in terms of choosing without replacement.  cK kℕ

theorem AlgebraicCombinatorics.FPS.antiNewtonBinomial.{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] [BinomialRingBinomialRing.{u_1} (R : Type u_1) [AddCommMonoid R] [Pow R ℕ] : Type u_1A binomial ring is a ring for which ascending Pochhammer evaluations are uniquely divisible by
suitable factorials. We define this notion as a mixin for additive commutative monoids with natural
number powers, but retain the ring name. We introduce `Ring.multichoose` as the uniquely defined
quotient.  KType u_1]
  [CharZeroCharZero.{u_1} (R : Type u_1) [AddMonoidWithOne R] : PropTypeclass for monoids with characteristic zero.
  (This is usually stated on fields but it makes sense for any additive monoid with 1.)

*Warning*: for a semiring `R`, `CharZero R` and `CharP R 0` need not coincide.
* `CharZero R` requires an injection `ℕ ↪ R`;
* `CharP R 0` asks that only `0 : ℕ` maps to `0 : R` under the map `ℕ → R`.
  For instance, endowing `{0, 1}` with addition given by `max` (i.e. `1` is absorbing), shows that
  `CharZero {0, 1}` does not hold and yet `CharP {0, 1} 0` does.
  This example is formalized in `Counterexamples/CharPZeroNeCharZero.lean`.
 KType u_1] (nK : KType u_1) :
  AlgebraicCombinatorics.FPS.fpsPowAlgebraicCombinatorics.FPS.fpsPow.{u_1} {K : Type u_1} [CommRing K] [Algebra ℚ K] (f : PowerSeries K) (c : K) :
  PowerSeries KThe c-th power of an FPS f with constant term 1.
f^c := Exp(c * Log(f)) = exp.subst (c * log_series.subst (f-1))
Label: def.fps.power-c 
      (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`. PowerSeries.XPowerSeries.X.{u_1} {R : Type u_1} [Semiring R] : PowerSeries RThe variable of the formal power series ring. )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`. (Neg.neg.{u} {α : Type u} [self : Neg α] : α → α`-a` computes the negative or opposite of `a`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `neg` (when used as a unary operator).-Neg.neg.{u} {α : Type u} [self : Neg α] : α → α`-a` computes the negative or opposite of `a`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `neg` (when used as a unary operator).nK)Neg.neg.{u} {α : Type u} [self : Neg α] : α → α`-a` computes the negative or opposite of `a`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `neg` (when used as a unary operator). =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.mkPowerSeries.mk.{u_2} {R : Type u_2} (f : ℕ → R) : PowerSeries RConstructor for formal power series.  fun iℕ ↦
      (-1) ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ`a ^ b` computes `a` to the power of `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `^` in identifiers is `pow`. iℕ *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`.
        Ring.chooseRing.choose.{u_1} {R : Type u_1} [AddCommGroupWithOne R] [Pow R ℕ] [BinomialRing R] (r : R) (n : ℕ) : RThe binomial coefficient `choose r n` generalizes the natural number `Nat.choose` function,
interpreted in terms of choosing without replacement.  (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).nK +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`. ↑iℕ -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). iℕ

theorem AlgebraicCombinatorics.FPS.one_fpsPow.{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] (cK : KType u_1) :
  AlgebraicCombinatorics.FPS.fpsPowAlgebraicCombinatorics.FPS.fpsPow.{u_1} {K : Type u_1} [CommRing K] [Algebra ℚ K] (f : PowerSeries K) (c : K) :
  PowerSeries KThe c-th power of an FPS f with constant term 1.
f^c := Exp(c * Log(f)) = exp.subst (c * log_series.subst (f-1))
Label: def.fps.power-c  1 cK =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 AlgebraicCombinatorics.FPS.constantCoeff_fpsPow.{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] {fPowerSeries K : PowerSeriesPowerSeries.{u_1} (R : Type u_1) : Type u_1Formal power series over a coefficient type `R`  KType u_1}
  (hfAlgebraicCombinatorics.FPS.HasConstantTermOne f :
    AlgebraicCombinatorics.FPS.HasConstantTermOneAlgebraicCombinatorics.FPS.HasConstantTermOne.{u_1} {K : Type u_1} [CommRing K] (f : PowerSeries K) : PropAn FPS has constant term 1.
This is the condition for f ∈ K⟦X⟧₁ in the source.
Label: def.fps.Exp-Log-maps (b)

Note: This is definitionally equivalent to membership in `PowerSeries₁` from ExpLog.lean:
`HasConstantTermOne f ↔ f ∈ PowerSeries₁`. The `Prop` form is used here for convenience
in hypotheses, while `PowerSeries₁` (a `Set`) is used in ExpLog.lean for subgroup structures. 
      fPowerSeries K)
  (cK : KType u_1) :
  PowerSeries.constantCoeffPowerSeries.constantCoeff.{u_1} {R : Type u_1} [Semiring R] : PowerSeries R →+* RThe constant coefficient of a formal power series. 
      (AlgebraicCombinatorics.FPS.fpsPowAlgebraicCombinatorics.FPS.fpsPow.{u_1} {K : Type u_1} [CommRing K] [Algebra ℚ K] (f : PowerSeries K) (c : K) :
  PowerSeries KThe c-th power of an FPS f with constant term 1.
f^c := Exp(c * Log(f)) = exp.subst (c * log_series.subst (f-1))
Label: def.fps.power-c  fPowerSeries K
        cK) =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