LaurentPolynomial.single_eq_C_mul_T
theorem LaurentPolynomial.single_eq_C_mul_T :
∀ {R : Type u_1} [inst : Semiring R] (r : R) (n : ℤ),
(fun₀ | n => r) = LaurentPolynomial.C r * LaurentPolynomial.T n
This theorem states that for any semiring `R`, and for any element `r` of `R` and integer `n`, the function mapping `n` to `r` is equivalent to the multiplication of the constant Laurent polynomial of `r` and the Laurent polynomial generated by `T` raised to the power `n`. In mathematical terms, this can be written as f(n) = r = C(r) * T^n, where f is a function, C is the constant Laurent polynomial, and T is the Laurent polynomial. This establishes a relationship between the definition of a constant Laurent polynomial, a Laurent polynomial generated by `T`, and a mapping from an integer to a constant of the semiring.
More concisely: For any semiring `R`, and any constant `r` in `R` and integer `n`, the function `r : ℤ → R` is equal to the constant Laurent polynomial `C(r)` multiplied by `T^n`, where `T` is a Laurent polynomial.
|
Polynomial.toLaurent_apply
theorem Polynomial.toLaurent_apply :
∀ {R : Type u_1} [inst : Semiring R] (p : Polynomial R),
Polynomial.toLaurent p = AddMonoidAlgebra.mapDomain Nat.cast p.toFinsupp
This theorem establishes the equivalence between the application of the function `Polynomial.toLaurent` to a polynomial `p` and the application of the function `AddMonoidAlgebra.mapDomain` with `Nat.cast` to the `toFinsupp` representation of the same polynomial `p`. Both functions take a polynomial with coefficients in `R` and transform it: `Polynomial.toLaurent` into a Laurent polynomial and `AddMonoidAlgebra.mapDomain` into an Additive Monoid Algebra, where `R` is a type equipped with a `Semiring` structure. This theorem is not marked as a simplification lemma as it's typically more convenient to use lemmas about `C` and `X` instead.
More concisely: The theorem asserts that applying `Polynomial.toLaurent` to a polynomial is equivalent to applying `AddMonoidAlgebra.mapDomain (Nat.cast)` to its `toFinsupp` representation.
|
Polynomial.toLaurent_C_mul_T
theorem Polynomial.toLaurent_C_mul_T :
∀ {R : Type u_1} [inst : Semiring R] (n : ℕ) (r : R),
Polynomial.toLaurent ((Polynomial.monomial n) r) = LaurentPolynomial.C r * LaurentPolynomial.T ↑n
The theorem `Polynomial.toLaurent_C_mul_T` states that for any semiring `R`, any natural number `n`, and any element `r` of `R`, the ring homomorphism converting a polynomial with coefficients in `R` to a Laurent polynomial with coefficients in `R` applied to the monomial `r * X^n` is equal to the product of the constant Laurent polynomial of `r` and the `n`th power of the variable of the Laurent polynomial. In other words, it expresses how monomials in the polynomial ring are converted to their counterparts in the Laurent polynomial ring.
More concisely: For any semiring R, the ring homomorphism from polynomials to Laurent polynomials maps r * X^n to r/1^n * X^n in the Laurent polynomial ring.
|
LaurentPolynomial.induction_on'
theorem LaurentPolynomial.induction_on' :
∀ {R : Type u_1} [inst : Semiring R] {M : LaurentPolynomial R → Prop} (p : LaurentPolynomial R),
(∀ (p q : LaurentPolynomial R), M p → M q → M (p + q)) →
(∀ (n : ℤ) (a : R), M (LaurentPolynomial.C a * LaurentPolynomial.T n)) → M p
The theorem `LaurentPolynomial.induction_on'` states that for any `R` of type `Type u_1` which is a semiring, and for any property `M` holding for Laurent polynomials over `R`, to prove that this property holds for an arbitrary Laurent polynomial `p`, it is sufficient to prove two conditions:
1. The property `M` is preserved under taking sums of Laurent polynomials. That is, if the property holds for polynomials `p` and `q`, then it also holds for the polynomial `p + q`.
2. The property `M` holds for any monomial of the Laurent polynomial, which can be expressed as a product of a constant `a` from `R` and `T` to the power of an integer `n`, where `T` is a function mapping integers to Laurent polynomials over `R`, and `C` is a ring homomorphism embedding `R` into the ring of Laurent polynomials over `R`.
More concisely: A property holding for Laurent polynomials over a semiring `R` can be proven for an arbitrary polynomial by showing it is preserved under summation and holds for each monomial, which is a product of a constant from `R` and a Laurent polynomial over `R` mapped by a ring homomorphism from `R` into the ring of Laurent polynomials over `R`.
|
LaurentPolynomial.mul_T_assoc
theorem LaurentPolynomial.mul_T_assoc :
∀ {R : Type u_1} [inst : Semiring R] (f : LaurentPolynomial R) (m n : ℤ),
f * LaurentPolynomial.T m * LaurentPolynomial.T n = f * LaurentPolynomial.T (m + n)
This theorem states that for any semiring `R`, Laurent polynomial `f` in `R` and integers `m` and `n`, the multiplication of `f` with `T` raised to the power of `m` and `n` respectively, is associative and can be simplified to the multiplication of `f` with `T` raised to the power of `m + n`. In the context of Laurent polynomials, this theorem provides a `simp` rule for the associativity of multiplication involving the terms of the form `T^n`, where `n` is an integer.
More concisely: For any semiring `R`, Laurent polynomial `f` in `R`, and integers `m` and `n`, the associativity holds between `(f * T^m) * T^n` and `f * T^(m + n)`.
|
Polynomial.toLaurent_C
theorem Polynomial.toLaurent_C :
∀ {R : Type u_1} [inst : Semiring R] (r : R), Polynomial.toLaurent (Polynomial.C r) = LaurentPolynomial.C r := by
sorry
This theorem states that for any semiring `R` and any element `r` of `R`, applying the function `Polynomial.C` to `r` to get a constant polynomial and then converting this polynomial to a Laurent polynomial using `Polynomial.toLaurent` is the same as directly mapping `r` to a constant Laurent polynomial using `LaurentPolynomial.C`. In other words, the process of converting a constant from `R` into a polynomial and then into a Laurent polynomial is equivalent to directly converting the constant into a Laurent polynomial.
More concisely: For any semiring `R` and its element `r`, `Polynomial.toLaurent (Polynomial.C r) = LaurentPolynomial.C r`.
|
LaurentPolynomial.C_eq_algebraMap
theorem LaurentPolynomial.C_eq_algebraMap :
∀ {R : Type u_2} [inst : CommSemiring R] (r : R), LaurentPolynomial.C r = (algebraMap R (LaurentPolynomial R)) r
The theorem `LaurentPolynomial.C_eq_algebraMap` states that, given a commutative semiring `R`, the function `C` (which embeds `R` into the ring of Laurent polynomials over `R` as the constant Laurent polynomials) is the same as the function `algebraMap R R[T;T⁻¹]` (which is an embedding induced by an algebra structure). However, it's important to note that while `C` is defined even when `R` is not necessarily commutative, `algebraMap` requires `R` to be a commutative semiring.
More concisely: Given a commutative semiring `R`, the constant embedding `C` of `R` into the ring of Laurent polynomials over `R` coincides with the algebra map `algebraMap R R[T;T⁻¹]`.
|
LaurentPolynomial.degree_C_mul_T
theorem LaurentPolynomial.degree_C_mul_T :
∀ {R : Type u_1} [inst : Semiring R] (n : ℤ) (a : R),
a ≠ 0 → (LaurentPolynomial.C a * LaurentPolynomial.T n).degree = ↑n
The theorem `LaurentPolynomial.degree_C_mul_T` states that for any semiring `R`, integer `n`, and non-zero element `a` of `R`, the degree of the product of the constant Laurent polynomial `a` and `T^n` (where 'degree' is defined as the maximum power of `T` in the Laurent polynomial, or negative infinity if the polynomial is zero) is equal to `n`. In other words, if you create a Laurent polynomial by multiplying a constant polynomial `a` by `T` raised to the power `n`, the highest power of `T` that appears in the resulting polynomial is `n`.
More concisely: For any semiring R, integer n, and non-zero element a in R, the degree of the Laurent polynomial a * T^n is equal to n.
|
LaurentPolynomial.T_zero
theorem LaurentPolynomial.T_zero : ∀ {R : Type u_1} [inst : Semiring R], LaurentPolynomial.T 0 = 1
This theorem states that for any semiring `R`, the `T` function of the Laurent Polynomial, when evaluated at 0, gives the value 1. Here, `LaurentPolynomial.T` is a function from integers to Laurent polynomials over `R`. It corresponds to the function `n ↦ T ^ n` in mathematics, but is defined in a different way due to technical reasons.
More concisely: For any semiring `R`, the value of the Laurent Polynomial `T` function evaluated at `0` is equal to `1`.
|
LaurentPolynomial.reduce_to_polynomial_of_mul_T
theorem LaurentPolynomial.reduce_to_polynomial_of_mul_T :
∀ {R : Type u_1} [inst : Semiring R] (f : LaurentPolynomial R) {Q : LaurentPolynomial R → Prop},
(∀ (f : Polynomial R), Q (Polynomial.toLaurent f)) →
(∀ (f : LaurentPolynomial R), Q (f * LaurentPolynomial.T 1) → Q f) → Q f
The theorem `LaurentPolynomial.reduce_to_polynomial_of_mul_T` states that if a property `Q` holds for all ordinary polynomials when viewed as Laurent polynomials, and if the property `Q` holds for a Laurent polynomial `f` whenever it holds for `f` multiplied by `T` (where `T` is a function representing the sequence `n ↦ T^n`), then this property `Q` is true for all Laurent polynomials. In the context of the theorem, `R` is a semiring and `f` is a Laurent polynomial over `R`. This is a kind of reduction property, allowing the analysis of Laurent polynomials to be reduced to the analysis of ordinary polynomials and their multiples by `T`.
More concisely: If a property holds for all Laurent polynomials that are ordinary polynomials, and it is preserved under multiplication by `T`, then the property holds for all Laurent polynomials over a semiring.
|
Polynomial.toLaurent_X_pow
theorem Polynomial.toLaurent_X_pow :
∀ {R : Type u_1} [inst : Semiring R] (n : ℕ), Polynomial.toLaurent (Polynomial.X ^ n) = LaurentPolynomial.T ↑n := by
sorry
This theorem establishes that for any semiring `R` and any natural number `n`, the ring homomorphism that takes a polynomial with coefficients in `R` to a Laurent polynomial, when applied to the `n`th power of the polynomial variable `X`, results in the `n`th element of the sequence `T` defined on the Laurent polynomial. In other words, the image of `X^n` under the polynomial to Laurent polynomial ring homomorphism is precisely `T^n`, where the power is interpreted in the integer sense. This relationship is fundamental in the manipulation and understanding of Laurent polynomials in terms of regular polynomials.
More concisely: For any semiring `R` and natural number `n`, the ring homomorphism from polynomials to Laurent polynomials maps `X^n` to `T^n`, where `T` is a fixed Laurent polynomial and the powers are taken in the integer sense.
|
LaurentPolynomial.toLaurent_support
theorem LaurentPolynomial.toLaurent_support :
∀ {R : Type u_1} [inst : Semiring R] (f : Polynomial R),
(Polynomial.toLaurent f).support = Finset.map Nat.castEmbedding f.support
This theorem, `LaurentPolynomial.toLaurent_support`, states that for any semiring `R` and a polynomial `f` with coefficients in `R`, the support (i.e., the set of indices with non-zero coefficients) of the Laurent polynomial equivalent of `f` (obtained using the function `Polynomial.toLaurent`) is the same as the support of `f`. However, it is viewed as a finset in the integers (`ℤ`) through the natural inclusion of natural numbers (`ℕ`) into integers, which is represented by the function `Nat.castEmbedding`. This embedding ensures that there are no duplicates in the resulting finset.
More concisely: The support of a polynomial's Laurent polynomial equivalent, as obtained by `Polynomial.toLaurent`, is equal to the support of the original polynomial viewed as a finset in integers through the natural embedding.
|
LaurentPolynomial.T_add
theorem LaurentPolynomial.T_add :
∀ {R : Type u_1} [inst : Semiring R] (m n : ℤ),
LaurentPolynomial.T (m + n) = LaurentPolynomial.T m * LaurentPolynomial.T n
This theorem states that for any semiring `R` and any two integers `m` and `n`, the function `LaurentPolynomial.T`, which maps an integer to a Laurent polynomial (a kind of polynomial that allows for negative exponents), satisfies the property that `T(m + n)` equals `T(m) * T(n)`. In other words, the function `LaurentPolynomial.T` is multiplicative with respect to integer addition, similar to properties of exponents in regular mathematics where `a^(m+n) = a^m * a^n`.
More concisely: For any semiring `R` and integers `m` and `n`, the function `LaurentPolynomial.T` satisfies `T(m + n) = T(m) * T(n)`.
|
LaurentPolynomial.ext
theorem LaurentPolynomial.ext :
∀ {R : Type u_1} [inst : Semiring R] {p q : LaurentPolynomial R}, (∀ (a : ℤ), p a = q a) → p = q
The theorem named `LaurentPolynomial.ext` states that, for every type `R` that is equipped with a semiring structure, any two Laurent polynomials `p` and `q` over `R` are equal if and only if their coefficients are equal at every integer `a`. In other words, two Laurent polynomials are identical when their corresponding coefficients for all integer powers of the indeterminate are identical.
More concisely: Two Laurent polynomials over a semiring are equal if and only if their coefficients at every integer power of the indeterminate are equal.
|
LaurentPolynomial.induction_on_mul_T
theorem LaurentPolynomial.induction_on_mul_T :
∀ {R : Type u_1} [inst : Semiring R] {Q : LaurentPolynomial R → Prop} (f : LaurentPolynomial R),
(∀ {f : Polynomial R} {n : ℕ}, Q (Polynomial.toLaurent f * LaurentPolynomial.T (-↑n))) → Q f
This theorem, `LaurentPolynomial.induction_on_mul_T`, is serving as an induction principle based on a multiplication operation in the context of Laurent polynomials. Given any type `R` that forms a semiring, and a proposition `Q` that applies to Laurent polynomials with coefficients in `R`, this theorem states that for any given Laurent polynomial `f`, if `Q` holds true for the product of the translation of any polynomial `f` from a regular polynomial space into the Laurent polynomial space and `T` raised to the power `-n` (where `n` is a natural number), then `Q` also holds true for the Laurent polynomial `f`. In simpler terms, if a property `Q` holds for all such products, it will hold for any given Laurent polynomial.
More concisely: If a property holds for the product of a Laurent polynomial and T^-n for all natural numbers n, then it holds for the given Laurent polynomial.
|