Polynomial.coe_C
theorem Polynomial.coe_C : ∀ {R : Type u_2} [inst : CommSemiring R] (a : R), ↑(Polynomial.C a) = (PowerSeries.C R) a
This theorem states that for any commutative semiring `R` and any element `a` from `R`, the result of applying the constant polynomial function `Polynomial.C` on `a` and then applying the coercion operation (denoted by ↑) is equal to the result of applying the constant power series function `PowerSeries.C` directly on `a`. In other words, the theorem asserts that the constant polynomial and the constant power series are semantically equivalent when operating on a given element from a commutative semiring.
More concisely: For any commutative semiring `R` and its element `a`, the constant polynomial function `Polynomial.C a` and the constant power series function `PowerSeries.C a` are equal when coerced to the same type.
|
PowerSeries.coeff_C
theorem PowerSeries.coeff_C :
∀ {R : Type u_1} [inst : Semiring R] (n : ℕ) (a : R),
(PowerSeries.coeff R n) ((PowerSeries.C R) a) = if n = 0 then a else 0
The theorem `PowerSeries.coeff_C` states that for any semiring `R`, any natural number `n`, and any element `a` of `R`, the `n`th coefficient of the constant formal power series generated by `a` is `a` if `n` is zero and zero otherwise. In other words, the only non-zero coefficient of a constant power series is the zeroth one, which is equal to the constant value `a` itself, and all other coefficients are zero.
More concisely: The constant formal power series generated by an element `a` in a semiring `R` has `a` as its zeroth coefficient and zero as all other coefficients.
|
PowerSeries.coeff_mul
theorem PowerSeries.coeff_mul :
∀ {R : Type u_1} [inst : Semiring R] (n : ℕ) (φ ψ : PowerSeries R),
(PowerSeries.coeff R n) (φ * ψ) =
(Finset.antidiagonal n).sum fun p => (PowerSeries.coeff R p.1) φ * (PowerSeries.coeff R p.2) ψ
This theorem, `PowerSeries.coeff_mul`, states that for any semiring `R`, and any natural number `n` and power series `φ` and `ψ` over `R`, the `n`th coefficient of the product of `φ` and `ψ` is equal to the sum, over all pairs `(i, j)` such that `i + j = n`, of the product of the `i`th coefficient of `φ` and the `j`th coefficient of `ψ`. This can be seen as a statement about how multiplication works in the ring of power series: it reflects the pattern of combining terms that we see when multiplying out expressions like `(a + b)(c + d)`.
More concisely: For any semiring `R`, natural number `n`, and power series `φ` and `ψ` over `R`, the `n`th coefficient of their product `φ * ψ` is equal to the sum, over all `i + j = n`, of the product of the `i`th coefficient of `φ` and the `j`th coefficient of `ψ`.
|
Polynomial.coe_monomial
theorem Polynomial.coe_monomial :
∀ {R : Type u_2} [inst : CommSemiring R] (n : ℕ) (a : R),
↑((Polynomial.monomial n) a) = (PowerSeries.monomial R n) a
The theorem `Polynomial.coe_monomial` states that for any given commutative semiring `R`, a natural number `n` and an element `a` of `R`, the coercion of the `n`-th monomial with coefficient `a` in the polynomial ring over `R` to a formal power series over `R` equals the `n`-th monomial with coefficient `a` in the formal power series ring over `R`. Essentially, this theorem is saying that the monomial structure in the polynomial ring and the formal power series ring over `R` is preserved under the coercion from polynomials to power series.
More concisely: For any commutative semiring R, the coercion of the n-th monomial with coefficient a in the polynomial ring over R to a formal power series over R equals the n-th monomial with coefficient a in the formal power series ring over R.
|
PowerSeries.coeff_one
theorem PowerSeries.coeff_one :
∀ {R : Type u_1} [inst : Semiring R] (n : ℕ), (PowerSeries.coeff R n) 1 = if n = 0 then 1 else 0
This theorem states that for any semiring `R` and any natural number `n`, the `n`th coefficient of the power series over `R` equals 1 if `n` equals 0 and otherwise it is 0. In other words, it specifies that the only non-zero coefficient in the power series is the one corresponding to `n` equals 0 and it is equal to 1, this power series represents the constant function with value 1.
More concisely: For any semiring `R`, the power series of the constant function 1 over `R` has exactly one non-zero coefficient, which is 1 at `n = 0`.
|
Polynomial.coe_inj
theorem Polynomial.coe_inj : ∀ {R : Type u_2} [inst : CommSemiring R] {φ ψ : Polynomial R}, ↑φ = ↑ψ ↔ φ = ψ
This theorem states that for any commutative semiring R, and any two polynomials φ and ψ over R, the coercion of φ to an expression is equal to the coercion of ψ to an expression if and only if φ is equal to ψ. In other words, the process of coercion preserves the equality of polynomials in the semiring.
More concisely: For any commutative semiring R, if two polynomials over R have the same coerced expressions, then they are equal.
|
PowerSeries.coeff_monomial
theorem PowerSeries.coeff_monomial :
∀ {R : Type u_1} [inst : Semiring R] (m n : ℕ) (a : R),
(PowerSeries.coeff R m) ((PowerSeries.monomial R n) a) = if m = n then a else 0
This theorem states that for any semiring `R`, and for any integers `m` and `n` and an element `a` of `R`, the `m`th coefficient of the `n`th monomial with coefficient `a` in the formal power series over `R` is `a` if `m` equals `n` and `0` otherwise. In other words, it's stating that in a power series, the coefficient for a given power is the value associated with that power in the monomial, and zero for all other powers.
More concisely: For any semiring `R`, the `m`th coefficient of the `n`th monomial with coefficient `a` in the formal power series over `R` is equal to `a` if `m = n`, and `0` otherwise.
|
PowerSeries.coeff_mk
theorem PowerSeries.coeff_mk :
∀ {R : Type u_1} [inst : Semiring R] (n : ℕ) (f : ℕ → R), (PowerSeries.coeff R n) (PowerSeries.mk f) = f n := by
sorry
The theorem `PowerSeries.coeff_mk` states that for any semiring `R`, any natural number `n`, and any function `f` from natural numbers to `R`, the `n`th coefficient of the formal power series constructed using function `f` is `f(n)`. This simply means that the power series created with `f` as the coefficient generating function accurately reflects the coefficients specified by `f`.
More concisely: For any semiring R, natural number n, and function f from natural numbers to R, the n-th coefficient of the power series formed from f is f(n).
|
PowerSeries.monomial_zero_eq_C_apply
theorem PowerSeries.monomial_zero_eq_C_apply :
∀ {R : Type u_1} [inst : Semiring R] (a : R), (PowerSeries.monomial R 0) a = (PowerSeries.C R) a
This theorem states that for any semiring `R` and any element `a` of this semiring, the zeroth monomial with coefficient `a` in the formal power series over `R` is equal to the constant formal power series with coefficient `a` over `R`. This means that both these power series representations, namely the zeroth monomial and the constant series, are equivalent when their coefficients are the same.
More concisely: For any semiring `R` and its element `a`, the zeroth monomial `x⁰` in the formal power series over `R` with coefficient `a` is equal to the constant formal power series over `R` with coefficient `a`. In other words, `x⁰ = ∑₀ i, a : R` in the formal power series over `R`.
|
PowerSeries.isUnit_constantCoeff
theorem PowerSeries.isUnit_constantCoeff :
∀ {R : Type u_1} [inst : Semiring R] (φ : PowerSeries R), IsUnit φ → IsUnit ((PowerSeries.constantCoeff R) φ) := by
sorry
This theorem states that if a formal power series over a coefficient type `R` (where `R` is a semiring) is a unit, meaning it has a two-sided inverse, then its constant coefficient is also a unit. In essence, if we have an invertible formal power series, its constant term is also invertible.
More concisely: If `f(x)` is a unit in the formal power series ring `R[x]` over a semiring `R`, then the constant coefficient `f(0)` is also a unit in `R`.
|
PowerSeries.coeff_X
theorem PowerSeries.coeff_X :
∀ {R : Type u_1} [inst : Semiring R] (n : ℕ), (PowerSeries.coeff R n) PowerSeries.X = if n = 1 then 1 else 0 := by
sorry
The theorem `PowerSeries.coeff_X` states that for any semiring `R` and natural number `n`, the `n`th coefficient of the formal power series variable in `R` is `1` if `n` equals `1`, and `0` otherwise. In other words, the only non-zero coefficient of the power series variable is the first one, corresponding to the fact that the power series for a variable `X` is simply `X` itself (which has coefficient `1` at the first power and `0` elsewhere).
More concisely: The power series expansion of a variable `X` in a semiring `R` has only a non-zero coefficient of `1` at the term `X^1`.
|
PowerSeries.ext
theorem PowerSeries.ext :
∀ {R : Type u_1} [inst : Semiring R] {φ ψ : PowerSeries R},
(∀ (n : ℕ), (PowerSeries.coeff R n) φ = (PowerSeries.coeff R n) ψ) → φ = ψ
This theorem states that for any semiring `R` and for any two formal power series `φ` and `ψ` in that semiring, if all the coefficients of `φ` and `ψ` are equal (i.e., for every natural number `n`, the `n`th coefficient of `φ` is equal to the `n`th coefficient of `ψ`), then `φ` and `ψ` are themselves equal. In other words, two formal power series are determined completely by their coefficients.
More concisely: If two formal power series over a semiring have equal coefficients for all natural numbers, then they are equal.
|
PowerSeries.coeff_zero_eq_constantCoeff_apply
theorem PowerSeries.coeff_zero_eq_constantCoeff_apply :
∀ {R : Type u_1} [inst : Semiring R] (φ : PowerSeries R),
(PowerSeries.coeff R 0) φ = (PowerSeries.constantCoeff R) φ
This theorem states that for any given power series φ over a coefficient type R, where R is a semiring, the 0th coefficient of the power series is equal to its constant coefficient. In more mathematical terms, if φ is a formal power series with coefficients in R, then the coefficient of x⁰ in φ, denoted as (PowerSeries.coeff R 0 φ), is the same as the constant term of φ, denoted as (PowerSeries.constantCoeff R φ).
More concisely: For any formal power series φ over a semiring R, the 0th coefficient equals the constant coefficient: (PowerSeries.coeff R 0 φ) = (PowerSeries.constantCoeff R φ).
|
PowerSeries.span_X_isPrime
theorem PowerSeries.span_X_isPrime :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R], (Ideal.span {PowerSeries.X}).IsPrime
This theorem states that for any commutative ring 'R' which is also an integral domain, the ideal generated by the variable of the power series ring over 'R' is a prime ideal. In other words, if we take the set containing just the variable of the power series ring and generate an ideal from it (using the span operation), this resulting ideal has the property of being prime. This is a fundamental property in the theory of commutative algebra related to power series.
More concisely: In a commutative ring that is an integral domain, the ideal generated by the power series ring's variable is a prime ideal.
|
PowerSeries.coeff_rescale
theorem PowerSeries.coeff_rescale :
∀ {R : Type u_1} [inst : CommSemiring R] (f : PowerSeries R) (a : R) (n : ℕ),
(PowerSeries.coeff R n) ((PowerSeries.rescale a) f) = a ^ n * (PowerSeries.coeff R n) f
This theorem states that for any commutative semiring `R`, any formal power series `f` over `R`, any element `a` of `R`, and any natural number `n`, the `n`-th coefficient of the rescaled power series `f(aX)` is equal to `a` to the power of `n` times the `n`-th coefficient of the original power series `f(X)`. In other words, rescaling a power series by a factor of `a` multiplies each coefficient of the power series by the corresponding power of `a`.
More concisely: For any commutative semiring `R`, any formal power series `f(X)` over `R`, and any element `a` in `R`, the `n`-th coefficient of the rescaled power series `f(aX)` equals `a^n` times the `n`-th coefficient of `f(X)`.
|
PowerSeries.coeff_C_mul
theorem PowerSeries.coeff_C_mul :
∀ {R : Type u_1} [inst : Semiring R] (n : ℕ) (φ : PowerSeries R) (a : R),
(PowerSeries.coeff R n) ((PowerSeries.C R) a * φ) = a * (PowerSeries.coeff R n) φ
This theorem states that for any semiring `R`, any natural number `n`, any formal power series `φ` over `R`, and any element `a` of the semiring `R`, the `n`th coefficient of the formal power series resulting from multiplying the constant formal power series generated by `a` and `φ`, is equal to `a` multiplied by the `n`th coefficient of `φ`. In mathematical terms, you can consider `PowerSeries.coeff R n` as a function extracting the `n`th coefficient from a formal power series, and `PowerSeries.C R` as a function creating a constant power series from a semiring element. The theorem then essentially states that these functions have a distributive-like property.
More concisely: For any semiring `R`, the `n`th coefficient of the product of the constant power series `PowerSeries.C R a` and formal power series `φ` over `R`, is equal to the product of element `a` and the `n`th coefficient of `φ`.
|
PowerSeries.coeff_zero_C
theorem PowerSeries.coeff_zero_C :
∀ {R : Type u_1} [inst : Semiring R] (a : R), (PowerSeries.coeff R 0) ((PowerSeries.C R) a) = a
This theorem states that for any semiring R and any element a of R, the nth coefficient of the constant formal power series of a (where n equals to zero), is a itself. In other words, when we construct a constant formal power series from an element a in the semiring R and then extract the 0th coefficient, we get back the original element a. It's essentially saying that the constant formal power series correctly embeds the semiring R into the ring of power series over R.
More concisely: For any semiring R and its element a, the constant formal power series of a equals a itself when the degree is zero.
|
Polynomial.coe_one
theorem Polynomial.coe_one : ∀ {R : Type u_2} [inst : CommSemiring R], ↑1 = 1
This theorem states that for any commutative semiring `R` of any type `u_2`, the coercion of the integer `1` to `R` is equal to the `1` in `R`. In other words, it asserts that casting `1` from an integer to any type in the commutative semiring results in the multiplicative identity of that semiring.
More concisely: For any commutative semiring R of type u\_2, the coercion of the integer 1 to R equals the multiplicative identity in R.
|
PowerSeries.eq_shift_mul_X_add_const
theorem PowerSeries.eq_shift_mul_X_add_const :
∀ {R : Type u_1} [inst : Semiring R] (φ : PowerSeries R),
φ =
(PowerSeries.mk fun p => (PowerSeries.coeff R (p + 1)) φ) * PowerSeries.X +
(PowerSeries.C R) ((PowerSeries.constantCoeff R) φ)
This theorem, `PowerSeries.eq_shift_mul_X_add_const`, states that for any formal power series `φ` over a semiring `R`, `φ` can be expressed as the sum of a term involving the variable of the formal power series (denoted as `PowerSeries.X`) and a constant term. Specifically, the term involving the variable is the product of `PowerSeries.X` and another power series created by shifting the coefficients of `φ` by one, i.e., the `n`th coefficient of this new series is the `(n+1)`th coefficient of `φ`. The constant term is obtained by applying `PowerSeries.C R` to the constant coefficient of `φ`, i.e., the 0th coefficient of `φ`. This is essentially the power series analogue of the property in algebra that every polynomial can be written as the product of x and a polynomial with lower degree plus a constant term.
More concisely: For any formal power series φ over a semiring R, there exists a constant c and a power series ψ such that φ = PowerSeries.X * ψ + c, where the coefficients of ψ are the shifted coefficients of φ.
|
PowerSeries.X_pow_eq
theorem PowerSeries.X_pow_eq :
∀ {R : Type u_1} [inst : Semiring R] (n : ℕ), PowerSeries.X ^ n = (PowerSeries.monomial R n) 1
This theorem states that for any semiring `R` and any natural number `n`, raising `X` of the formal power series ring to the `n`th power is equal to the `n`th monomial with coefficient 1 in `R`. In other words, $(X^n)$ in the formal power series ring is the same as the `n`th monomial where the coefficient is 1.
More concisely: For any semiring `R` and natural number `n`, the `n`th power of `X` in the formal power series ring equals the `n`th monomial with coefficient 1 in `R`.
|
PowerSeries.eq_X_mul_shift_add_const
theorem PowerSeries.eq_X_mul_shift_add_const :
∀ {R : Type u_1} [inst : Semiring R] (φ : PowerSeries R),
φ =
(PowerSeries.X * PowerSeries.mk fun p => (PowerSeries.coeff R (p + 1)) φ) +
(PowerSeries.C R) ((PowerSeries.constantCoeff R) φ)
The theorem `PowerSeries.eq_X_mul_shift_add_const` states that for any type `R` equipped with a semiring structure and for any formal power series `φ` over `R`, we can decompose `φ` into a sum of two parts: the first part is the product of the formal power series variable `X` and a new formal power series obtained by shifting the coefficients of `φ` by one, and the second part is the constant formal power series obtained from the constant coefficient of `φ`. In mathematical notation, it can be written as:
For any φ, φ = X * Σ (aₙ₊₁Xⁿ) + a₀, where aₙ are the coefficients of φ.
More concisely: For any formal power series φ over a semiring R, φ equals the product of X and the shifted series of φ's coefficients, plus the constant series represented by φ's constant term.
|
Polynomial.coeff_coe
theorem Polynomial.coeff_coe :
∀ {R : Type u_2} [inst : CommSemiring R] (φ : Polynomial R) (n : ℕ), (PowerSeries.coeff R n) ↑φ = φ.coeff n := by
sorry
This theorem, `Polynomial.coeff_coe`, asserts that for any commutative semiring `R`, any polynomial `φ` defined over `R`, and any natural number `n`, the `n`th coefficient of the power series obtained from `φ` (obtained by treating `φ` as a power series and finding its `n`th coefficient) is equal to the `n`th coefficient of the polynomial `φ`. In other words, the process of converting a polynomial to a power series does not change its coefficients.
More concisely: For any commutative semiring R, polynomial φ over R, and natural number n, the n-th coefficient of the power series expansion of φ is equal to the n-th coefficient of φ itself.
|
PowerSeries.constantCoeff_X
theorem PowerSeries.constantCoeff_X :
∀ {R : Type u_1} [inst : Semiring R], (PowerSeries.constantCoeff R) PowerSeries.X = 0
The theorem `PowerSeries.constantCoeff_X` states that for any semiring `R`, the constant coefficient of the formal power series variable in `R` (often denoted as `X`) is zero. In other words, when we extract the constant coefficient (the zero-degree term) from the power series for the variable, we get zero, as there are no terms without the variable in the formal power series for `X`.
More concisely: The constant coefficient of the formal power series variable is zero in any semiring.
|
PowerSeries.coeff_X_pow
theorem PowerSeries.coeff_X_pow :
∀ {R : Type u_1} [inst : Semiring R] (m n : ℕ),
(PowerSeries.coeff R m) (PowerSeries.X ^ n) = if m = n then 1 else 0
This theorem pertains to the coefficients of a formal power series over a semiring. Specifically, for any semiring `R` and any natural numbers `m` and `n`, it states that the `m`th coefficient of the `n`th power of the power series variable (denoted by `PowerSeries.X ^ n`) is `1` if `m` is equal to `n`, and `0` otherwise. This theorem characterizes a significant property of formal power series, which parallels the similar property of monomials in polynomial rings, where the coefficient of `x^n` in `x^m` is `1` when `m = n` and `0` otherwise.
More concisely: For any semiring `R`, the `m`th coefficient of `PowerSeries.X ^ n` is `1` if `m = n`, and `0` otherwise.
|
PowerSeries.coeff_zero_eq_constantCoeff
theorem PowerSeries.coeff_zero_eq_constantCoeff :
∀ {R : Type u_1} [inst : Semiring R], ⇑(PowerSeries.coeff R 0) = ⇑(PowerSeries.constantCoeff R)
This theorem states that for any semiring `R`, the zeroth coefficient of a formal power series in `R` is equal to the constant coefficient of that power series in `R`. In other words, when we apply the `PowerSeries.coeff R 0` function or the `PowerSeries.constantCoeff R` function to a power series, we get the same result, which is the constant term of the power series. This theorem is valid in the context of any semiring, a type of algebraic structure that extends the concept of a ring by allowing multiplication to be commutative.
More concisely: For any semiring `R`, the zeroth coefficient of a power series in `R` equals its constant coefficient.
|
PowerSeries.ext_iff
theorem PowerSeries.ext_iff :
∀ {R : Type u_1} [inst : Semiring R] {φ ψ : PowerSeries R},
φ = ψ ↔ ∀ (n : ℕ), (PowerSeries.coeff R n) φ = (PowerSeries.coeff R n) ψ
This theorem states that for any semiring `R` and any two formal power series `φ` and `ψ` over `R`, `φ` and `ψ` are equal if and only if all of their coefficients are equal. In other words, the equality of two power series is determined by the equality of their corresponding coefficients at every non-negative integer index `n`.
More concisely: For any semiring `R` and formal power series `φ` and `ψ` over `R`, `φ = ψ` if and only if `φ(n) = ψ(n)` for all non-negative integers `n`.
|
PowerSeries.X_prime
theorem PowerSeries.X_prime : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R], Prime PowerSeries.X := by
sorry
This theorem states that the indeterminate ("variable") of the power series ring over an integral domain is prime. In other words, for any commutative ring `R` that is also an integral domain, the power series generator `X` is a prime element. This means that `X` is not zero, is not a unit (cannot be inverted), and if `X` divides the product of two power series, then `X` must divide at least one of them.
More concisely: In an integral domain `R`, the power series generator `X` of the power series ring over `R` is a prime element.
|