theorem FPS.isPolynomial_iff_exists_degree_bound.{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 : PowerSeriesPowerSeries.{u_1} (R : Type u_1) : Type u_1Formal power series over a coefficient type `R`  KType u_1) :
  FPS.IsPolynomialFPS.IsPolynomial.{u_1} {K : Type u_1} [CommRing K] (f : PowerSeries K) : PropA power series is a polynomial if it has finite support, i.e., only finitely many
nonzero coefficients. This corresponds to Definition 7.5.1 (def.fps.pol) in the source.  fPowerSeries K ↔Iff (a b : Prop) : PropIf and only if, or logical bi-implication. `a ↔ b` means that `a` implies `b` and vice versa.
By `propext`, this implies that `a` and `b` are equal and hence any expression involving `a`
is equivalent to the corresponding expression with `b` instead.


Conventions for notations in identifiers:

 * The recommended spelling of `↔` in identifiers is `iff`.

 * The recommended spelling of `<->` in identifiers is `iff` (prefer `↔` over `<->`).
    ∃ Nℕ,
      ∀ nℕ ≥ Nℕ, (PowerSeries.coeffPowerSeries.coeff.{u_1} {R : Type u_1} [Semiring R] (n : ℕ) : PowerSeries R →ₗ[R] RThe `n`th coefficient of a formal power series.  nℕ) 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 FPS.isPolynomial_iff_exists_polynomial.{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 : PowerSeriesPowerSeries.{u_1} (R : Type u_1) : Type u_1Formal power series over a coefficient type `R`  KType u_1) :
  FPS.IsPolynomialFPS.IsPolynomial.{u_1} {K : Type u_1} [CommRing K] (f : PowerSeries K) : PropA power series is a polynomial if it has finite support, i.e., only finitely many
nonzero coefficients. This corresponds to Definition 7.5.1 (def.fps.pol) in the source.  fPowerSeries K ↔Iff (a b : Prop) : PropIf and only if, or logical bi-implication. `a ↔ b` means that `a` implies `b` and vice versa.
By `propext`, this implies that `a` and `b` are equal and hence any expression involving `a`
is equivalent to the corresponding expression with `b` instead.


Conventions for notations in identifiers:

 * The recommended spelling of `↔` in identifiers is `iff`.

 * The recommended spelling of `<->` in identifiers is `iff` (prefer `↔` over `<->`). ∃ pPolynomial 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`. ↑pPolynomial K

theorem FPS.isPolynomial_of_polynomial.{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]
  (pPolynomial K : PolynomialPolynomial.{u_1} (R : Type u_1) [Semiring R] : Type u_1`Polynomial R` is the type of univariate polynomials over `R`,
denoted as `R[X]` within the `Polynomial` namespace.

Polynomials should be seen as (semi-)rings with the additional constructor `X`.
The embedding from `R` is called `C`.  KType u_1) : FPS.IsPolynomialFPS.IsPolynomial.{u_1} {K : Type u_1} [CommRing K] (f : PowerSeries K) : PropA power series is a polynomial if it has finite support, i.e., only finitely many
nonzero coefficients. This corresponds to Definition 7.5.1 (def.fps.pol) in the source.  ↑pPolynomial K

theorem FPS.coe_toPolynomial.{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 : PowerSeriesPowerSeries.{u_1} (R : Type u_1) : Type u_1Formal power series over a coefficient type `R`  KType u_1)
  (hfFPS.IsPolynomial f : FPS.IsPolynomialFPS.IsPolynomial.{u_1} {K : Type u_1} [CommRing K] (f : PowerSeries K) : PropA power series is a polynomial if it has finite support, i.e., only finitely many
nonzero coefficients. This corresponds to Definition 7.5.1 (def.fps.pol) in the source.  fPowerSeries K) :
  ↑(FPS.toPolynomialFPS.toPolynomial.{u_1} {K : Type u_1} [CommRing K] (f : PowerSeries K) (hf : FPS.IsPolynomial f) : Polynomial KConvert a polynomial power series to its corresponding polynomial.
This requires a proof that the power series is a polynomial.  fPowerSeries K hfFPS.IsPolynomial f) =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 FPS.toPolynomial_coe.{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] (pPolynomial K : PolynomialPolynomial.{u_1} (R : Type u_1) [Semiring R] : Type u_1`Polynomial R` is the type of univariate polynomials over `R`,
denoted as `R[X]` within the `Polynomial` namespace.

Polynomials should be seen as (semi-)rings with the additional constructor `X`.
The embedding from `R` is called `C`.  KType u_1) :
  FPS.toPolynomialFPS.toPolynomial.{u_1} {K : Type u_1} [CommRing K] (f : PowerSeries K) (hf : FPS.IsPolynomial f) : Polynomial KConvert a polynomial power series to its corresponding polynomial.
This requires a proof that the power series is a polynomial.  ↑pPolynomial 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`. pPolynomial K

theorem FPS.isPolynomial_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] : FPS.IsPolynomialFPS.IsPolynomial.{u_1} {K : Type u_1} [CommRing K] (f : PowerSeries K) : PropA power series is a polynomial if it has finite support, i.e., only finitely many
nonzero coefficients. This corresponds to Definition 7.5.1 (def.fps.pol) in the source.  0

theorem FPS.isPolynomial_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] : FPS.IsPolynomialFPS.IsPolynomial.{u_1} {K : Type u_1} [CommRing K] (f : PowerSeries K) : PropA power series is a polynomial if it has finite support, i.e., only finitely many
nonzero coefficients. This corresponds to Definition 7.5.1 (def.fps.pol) in the source.  1

theorem FPS.isPolynomial_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] {fPowerSeries K gPowerSeries K : PowerSeriesPowerSeries.{u_1} (R : Type u_1) : Type u_1Formal power series over a coefficient type `R`  KType u_1}
  (hfFPS.IsPolynomial f : FPS.IsPolynomialFPS.IsPolynomial.{u_1} {K : Type u_1} [CommRing K] (f : PowerSeries K) : PropA power series is a polynomial if it has finite support, i.e., only finitely many
nonzero coefficients. This corresponds to Definition 7.5.1 (def.fps.pol) in the source.  fPowerSeries K)
  (hgFPS.IsPolynomial g : FPS.IsPolynomialFPS.IsPolynomial.{u_1} {K : Type u_1} [CommRing K] (f : PowerSeries K) : PropA power series is a polynomial if it has finite support, i.e., only finitely many
nonzero coefficients. This corresponds to Definition 7.5.1 (def.fps.pol) in the source.  gPowerSeries K) :
  FPS.IsPolynomialFPS.IsPolynomial.{u_1} {K : Type u_1} [CommRing K] (f : PowerSeries K) : PropA power series is a polynomial if it has finite support, i.e., only finitely many
nonzero coefficients. This corresponds to Definition 7.5.1 (def.fps.pol) in the source.  (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`.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`. 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`.

theorem FPS.isPolynomial_neg.{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 : PowerSeriesPowerSeries.{u_1} (R : Type u_1) : Type u_1Formal power series over a coefficient type `R`  KType u_1}
  (hfFPS.IsPolynomial f : FPS.IsPolynomialFPS.IsPolynomial.{u_1} {K : Type u_1} [CommRing K] (f : PowerSeries K) : PropA power series is a polynomial if it has finite support, i.e., only finitely many
nonzero coefficients. This corresponds to Definition 7.5.1 (def.fps.pol) in the source.  fPowerSeries K) :
  FPS.IsPolynomialFPS.IsPolynomial.{u_1} {K : Type u_1} [CommRing K] (f : PowerSeries K) : PropA power series is a polynomial if it has finite support, i.e., only finitely many
nonzero coefficients. This corresponds to Definition 7.5.1 (def.fps.pol) in the source.  (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).fPowerSeries K)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).

theorem FPS.isPolynomial_sub.{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}
  (hfFPS.IsPolynomial f : FPS.IsPolynomialFPS.IsPolynomial.{u_1} {K : Type u_1} [CommRing K] (f : PowerSeries K) : PropA power series is a polynomial if it has finite support, i.e., only finitely many
nonzero coefficients. This corresponds to Definition 7.5.1 (def.fps.pol) in the source.  fPowerSeries K)
  (hgFPS.IsPolynomial g : FPS.IsPolynomialFPS.IsPolynomial.{u_1} {K : Type u_1} [CommRing K] (f : PowerSeries K) : PropA power series is a polynomial if it has finite support, i.e., only finitely many
nonzero coefficients. This corresponds to Definition 7.5.1 (def.fps.pol) in the source.  gPowerSeries K) :
  FPS.IsPolynomialFPS.IsPolynomial.{u_1} {K : Type u_1} [CommRing K] (f : PowerSeries K) : PropA power series is a polynomial if it has finite support, i.e., only finitely many
nonzero coefficients. This corresponds to Definition 7.5.1 (def.fps.pol) in the source.  (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). gPowerSeries 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).

theorem FPS.isPolynomial_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}
  (hfFPS.IsPolynomial f : FPS.IsPolynomialFPS.IsPolynomial.{u_1} {K : Type u_1} [CommRing K] (f : PowerSeries K) : PropA power series is a polynomial if it has finite support, i.e., only finitely many
nonzero coefficients. This corresponds to Definition 7.5.1 (def.fps.pol) in the source.  fPowerSeries K)
  (hgFPS.IsPolynomial g : FPS.IsPolynomialFPS.IsPolynomial.{u_1} {K : Type u_1} [CommRing K] (f : PowerSeries K) : PropA power series is a polynomial if it has finite support, i.e., only finitely many
nonzero coefficients. This corresponds to Definition 7.5.1 (def.fps.pol) in the source.  gPowerSeries K) :
  FPS.IsPolynomialFPS.IsPolynomial.{u_1} {K : Type u_1} [CommRing K] (f : PowerSeries K) : PropA power series is a polynomial if it has finite support, i.e., only finitely many
nonzero coefficients. This corresponds to Definition 7.5.1 (def.fps.pol) in the source.  (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 FPS.isPolynomial_smul.{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 : PowerSeriesPowerSeries.{u_1} (R : Type u_1) : Type u_1Formal power series over a coefficient type `R`  KType u_1} (cK : KType u_1)
  (hfFPS.IsPolynomial f : FPS.IsPolynomialFPS.IsPolynomial.{u_1} {K : Type u_1} [CommRing K] (f : PowerSeries K) : PropA power series is a polynomial if it has finite support, i.e., only finitely many
nonzero coefficients. This corresponds to Definition 7.5.1 (def.fps.pol) in the source.  fPowerSeries K) :
  FPS.IsPolynomialFPS.IsPolynomial.{u_1} {K : Type u_1} [CommRing K] (f : PowerSeries K) : PropA power series is a polynomial if it has finite support, i.e., only finitely many
nonzero coefficients. This corresponds to Definition 7.5.1 (def.fps.pol) in the source.  (HSMul.hSMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSMul α β γ] : α → β → γ`a • b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent, but it is intended to be used for left actions. 

Conventions for notations in identifiers:

 * The recommended spelling of `•` in identifiers is `smul`.cK •HSMul.hSMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSMul α β γ] : α → β → γ`a • b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent, but it is intended to be used for left actions. 

Conventions for notations in identifiers:

 * The recommended spelling of `•` in identifiers is `smul`. fPowerSeries K)HSMul.hSMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSMul α β γ] : α → β → γ`a • b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent, but it is intended to be used for left actions. 

Conventions for notations in identifiers:

 * The recommended spelling of `•` in identifiers is `smul`.

theorem FPS.isPolynomial_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] :
  FPS.IsPolynomialFPS.IsPolynomial.{u_1} {K : Type u_1} [CommRing K] (f : PowerSeries K) : PropA power series is a polynomial if it has finite support, i.e., only finitely many
nonzero coefficients. This corresponds to Definition 7.5.1 (def.fps.pol) in the source.  PowerSeries.XPowerSeries.X.{u_1} {R : Type u_1} [Semiring R] : PowerSeries RThe variable of the formal power series ring. 

theorem FPS.isPolynomial_C.{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] (cK : KType u_1) :
  FPS.IsPolynomialFPS.IsPolynomial.{u_1} {K : Type u_1} [CommRing K] (f : PowerSeries K) : PropA power series is a polynomial if it has finite support, i.e., only finitely many
nonzero coefficients. This corresponds to Definition 7.5.1 (def.fps.pol) in the source.  (PowerSeries.CPowerSeries.C.{u_1} {R : Type u_1} [Semiring R] : R →+* PowerSeries RThe constant formal power series.  cK)

theorem FPS.ring_add_assoc.{u_2} {RType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [RingRing.{u} (R : Type u) : Type uA `Ring` is a `Semiring` with negation making it an additive group.  RType u_2] (aR bR cR : RType u_2) :
  aR +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`. (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`.bR +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`. cR)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`. aR +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`. bR +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`. cR

theorem FPS.ring_add_comm.{u_2} {RType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [RingRing.{u} (R : Type u) : Type uA `Ring` is a `Semiring` with negation making it an additive group.  RType u_2] (aR bR : RType u_2) : aR +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`. bR =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`. bR +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`. aR

theorem FPS.ring_add_zero.{u_2} {RType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [RingRing.{u} (R : Type u) : Type uA `Ring` is a `Semiring` with negation making it an additive group.  RType u_2] (aR : RType u_2) : aR +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`. 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`. aR

theorem FPS.ring_zero_add.{u_2} {RType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [RingRing.{u} (R : Type u) : Type uA `Ring` is a `Semiring` with negation making it an additive group.  RType u_2] (aR : RType u_2) : 0 +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`. aR =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`. aR

theorem FPS.ring_add_neg.{u_2} {RType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [RingRing.{u} (R : Type u) : Type uA `Ring` is a `Semiring` with negation making it an additive group.  RType u_2] (aR : RType u_2) : aR +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).aR =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 FPS.ring_mul_assoc.{u_2} {RType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [RingRing.{u} (R : Type u) : Type uA `Ring` is a `Semiring` with negation making it an additive group.  RType u_2] (aR bR cR : RType u_2) :
  aR *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`. (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`.bR *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`. cR)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`. aR *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`. bR *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`. cR

theorem FPS.ring_left_distrib.{u_2} {RType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [RingRing.{u} (R : Type u) : Type uA `Ring` is a `Semiring` with negation making it an additive group.  RType u_2] (aR bR cR : RType u_2) :
  aR *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`. (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`.bR +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`. cR)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`. aR *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`. bR +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`. aR *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`. cR

theorem FPS.ring_right_distrib.{u_2}
  {RType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [RingRing.{u} (R : Type u) : Type uA `Ring` is a `Semiring` with negation making it an additive group.  RType u_2] (aR bR cR : RType u_2) :
  (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`.aR +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`. bR)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`. cR =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`. aR *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`. cR +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`. bR *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`. cR

theorem FPS.ring_mul_one.{u_2} {RType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [RingRing.{u} (R : Type u) : Type uA `Ring` is a `Semiring` with negation making it an additive group.  RType u_2] (aR : RType u_2) : aR *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`. 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`. aR

theorem FPS.ring_one_mul.{u_2} {RType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [RingRing.{u} (R : Type u) : Type uA `Ring` is a `Semiring` with negation making it an additive group.  RType u_2] (aR : RType u_2) : 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`. aR =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`. aR

theorem FPS.ring_mul_zero.{u_2} {RType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [RingRing.{u} (R : Type u) : Type uA `Ring` is a `Semiring` with negation making it an additive group.  RType u_2] (aR : RType u_2) : aR *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`. 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`. 0

theorem FPS.ring_zero_mul.{u_2} {RType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [RingRing.{u} (R : Type u) : Type uA `Ring` is a `Semiring` with negation making it an additive group.  RType u_2] (aR : RType u_2) : 0 *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`. aR =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 FPS.kalg_add_comm.{u_2} {AType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [RingRing.{u} (R : Type u) : Type uA `Ring` is a `Semiring` with negation making it an additive group.  AType u_2] (aA bA : AType u_2) : aA +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`. bA =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`. bA +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`. aA

theorem FPS.kalg_add_assoc.{u_2} {AType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [RingRing.{u} (R : Type u) : Type uA `Ring` is a `Semiring` with negation making it an additive group.  AType u_2] (aA bA cA : AType u_2) :
  aA +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`. (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`.bA +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`. cA)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`. aA +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`. bA +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`. cA

theorem FPS.kalg_add_zero.{u_2} {AType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [RingRing.{u} (R : Type u) : Type uA `Ring` is a `Semiring` with negation making it an additive group.  AType u_2] (aA : AType u_2) : aA +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`. 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`. aA

theorem FPS.kalg_mul_assoc.{u_2} {AType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [RingRing.{u} (R : Type u) : Type uA `Ring` is a `Semiring` with negation making it an additive group.  AType u_2] (aA bA cA : AType u_2) :
  aA *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`. (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`.bA *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`. cA)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`. aA *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`. bA *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`. cA

theorem FPS.kalg_left_distrib.{u_2} {AType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [RingRing.{u} (R : Type u) : Type uA `Ring` is a `Semiring` with negation making it an additive group.  AType u_2] (aA bA cA : AType u_2) :
  aA *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`. (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`.bA +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`. cA)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`. aA *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`. bA +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`. aA *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`. cA