HahnSeries.single_coeff_same
theorem HahnSeries.single_coeff_same :
∀ {Γ : Type u_1} {R : Type u_2} [inst : PartialOrder Γ] [inst_1 : Zero R] (a : Γ) (r : R),
((HahnSeries.single a) r).coeff a = r
The theorem `HahnSeries.single_coeff_same` asserts that for any types `Γ` and `R` with a partial order on `Γ` and a zero element in `R`, and for any elements `a` of type `Γ` and `r` of type `R`, the coefficient of `a` in the Hahn series generated by the `single` function with inputs `a` and `r` is `r`. In other words, the function `HahnSeries.single a r` creates a Hahn series where the coefficient of `a` is `r`, and this theorem confirms that.
More concisely: For any type `Γ` with a partial order and a zero element, and for any `a ∈ Γ` and `r ∈ R`, the coefficient of `a` in the Hahn series generated by `HahnSeries.single a r` is equal to `r`.
|
HahnSeries.zero_coeff
theorem HahnSeries.zero_coeff :
∀ {Γ : Type u_1} {R : Type u_2} [inst : PartialOrder Γ] [inst_1 : Zero R] {a : Γ}, HahnSeries.coeff 0 a = 0 := by
sorry
The theorem `HahnSeries.zero_coeff` states that for any given types `Γ` and `R`, where `Γ` is a partial order and `R` is a zero object, the coefficient of any element `a` of type `Γ` in the zero Hahn series is zero. In other words, the zero Hahn series has all its coefficients equal to zero.
More concisely: For any partial order `Γ` and zero object `R`, the zero Hahn series has all coefficients equal to zero.
|
HahnSeries.embDomain_coeff
theorem HahnSeries.embDomain_coeff :
∀ {Γ : Type u_1} {R : Type u_2} [inst : PartialOrder Γ] [inst_1 : Zero R] {Γ' : Type u_3} [inst_2 : PartialOrder Γ']
{f : Γ ↪o Γ'} {x : HahnSeries Γ R} {a : Γ}, (HahnSeries.embDomain f x).coeff (f a) = x.coeff a
The theorem `HahnSeries.embDomain_coeff` states that for every ordered types `Γ` and `Γ'`, every type `R` equipped with an zero element, every order embedding `f` from `Γ` to `Γ'`, every Hahn series `x` over `Γ` and `R`, and every element `a` of `Γ`, the coefficient of the image of `a` under `f` in the Hahn series obtained by extending the domain of `x` by `f` is the same as the coefficient of `a` in `x`. This property maintains the coefficients of elements from the original domain in the new, extended domain.
More concisely: For every Hahn series $x$ over ordered types $\Gamma$ and a ring $R$, and an order embedding $f$ from $\Gamma$ to $\Gamma'$, the coefficient of $f(a)$ in the extended Hahn series is equal to the coefficient of $a$ in $x$, for all $a\in \Gamma$.
|
HahnSeries.order_zero
theorem HahnSeries.order_zero :
∀ {Γ : Type u_1} {R : Type u_2} [inst : PartialOrder Γ] [inst_1 : Zero R] [inst_2 : Zero Γ],
HahnSeries.order 0 = 0
This theorem states that, for any types `Γ` and `R` where `Γ` is a partial order and `R` and `Γ` have a zero element, the order of the zero Hahn Series is indeed zero. In other words, it confirms that our definition of `HahnSeries.order` correctly assigns an order of zero to the zero Hahn Series.
More concisely: For any partial order types `Γ` with a zero element, the order of the zero Hahn series in `Γ` is zero.
|
HahnSeries.coeff_order_ne_zero
theorem HahnSeries.coeff_order_ne_zero :
∀ {Γ : Type u_1} {R : Type u_2} [inst : PartialOrder Γ] [inst_1 : Zero R] [inst_2 : Zero Γ] {x : HahnSeries Γ R},
x ≠ 0 → x.coeff x.order ≠ 0
The theorem `HahnSeries.coeff_order_ne_zero` states that for any Hahn series `x`, if `x` is not equal to zero, then the coefficient of `x` at its order, denoted by `HahnSeries.order x`, is not zero. Therefore, the theorem asserts that the non-zero Hahn series `x` will always have a non-zero coefficient at the order of the Hahn series.
More concisely: If a Hahn series is non-zero, then its coefficient at the order of the series is non-zero.
|
HahnSeries.support_zero
theorem HahnSeries.support_zero :
∀ {Γ : Type u_1} {R : Type u_2} [inst : PartialOrder Γ] [inst_1 : Zero R], HahnSeries.support 0 = ∅
This theorem states that for any types `Γ` and `R`, where `Γ` is a partially ordered set and `R` has a zero element, the support of a zero Hahn series is an empty set. In other words, the set of indices whose coefficients are nonzero in a zero Hahn series is empty, since all coefficients in a zero Hahn series are zero.
More concisely: For any partially ordered set Γ and type R with a zero element, the coefficients of a zero Hahn series over (Γ, R) are all zero, implying an empty support.
|
HahnSeries.mem_support
theorem HahnSeries.mem_support :
∀ {Γ : Type u_1} {R : Type u_2} [inst : PartialOrder Γ] [inst_1 : Zero R] (x : HahnSeries Γ R) (a : Γ),
a ∈ x.support ↔ x.coeff a ≠ 0
The theorem `HahnSeries.mem_support` states that for any given types `Γ` and `R`, where `Γ` has a partial order and `R` has a zero element, and for any Hahn Series `x` of type `HahnSeries Γ R` and any element `a` of type `Γ`, `a` is in the support of the Hahn Series `x` if and only if the coefficient of `a` in `x` is not equal to zero. In other words, the support of a Hahn Series is precisely the set of indices whose corresponding coefficients in the series are non-zero.
More concisely: The support of a Hahn Series over a partially ordered type and a ring with zero element equals the set of indices corresponding to non-zero coefficients.
|
Mathlib.RingTheory.HahnSeries.Basic._auxLemma.4
theorem Mathlib.RingTheory.HahnSeries.Basic._auxLemma.4 :
∀ {Γ : Type u_1} {R : Type u_2} [inst : PartialOrder Γ] [inst_1 : Zero R] (x : HahnSeries Γ R) (a : Γ),
(a ∈ x.support) = (x.coeff a ≠ 0)
The theorem, `Mathlib.RingTheory.HahnSeries.Basic._auxLemma.4`, states that for any types Γ and R, where Γ has a partial order and R has a zero, and for any Hahn series `x` of type `HahnSeries Γ R` and any element `a` of Γ, `a` is in the support of `x` if and only if the coefficient of `a` in `x` is non-zero. In other words, the support of a Hahn series is precisely the set of indices at which the series has non-zero coefficients.
More concisely: For any Hahn series $x$ over a poset $\Gamma$ with values in a ring $R$, the index $a \in \Gamma$ is in the support of $x$ if and only if the coefficient of $a$ in $x$ is non-zero.
|
HahnSeries.order_of_ne
theorem HahnSeries.order_of_ne :
∀ {Γ : Type u_1} {R : Type u_2} [inst : PartialOrder Γ] [inst_1 : Zero R] [inst_2 : Zero Γ] {x : HahnSeries Γ R}
(hx : x ≠ 0), x.order = ⋯.min ⋯
The theorem `HahnSeries.order_of_ne` states that for any Hahn series `x` of type `HahnSeries Γ R` where `Γ` is a type with a partial order, `R` is a type with a zero element, and `x` is not equal to zero, the order of `x` is equal to the minimum element of a certain well-founded set. Here, the order of a Hahn series is defined as the minimal element of `Γ` at which the series has a nonzero coefficient, and the `Set.IsWF.min` function returns a minimal element of a nonempty well-founded set.
More concisely: The order of a nonzero Hahn series `x` over a type `Γ` with a partial order and `R` with a zero element is equal to the minimum element in `Γ` where `x` has a nonzero coefficient.
|
HahnSeries.ext_iff
theorem HahnSeries.ext_iff :
∀ {Γ : Type u_1} {R : Type u_2} {inst : PartialOrder Γ} {inst_1 : Zero R} (x y : HahnSeries Γ R),
x = y ↔ x.coeff = y.coeff
This theorem states that for any two Hahn series `x` and `y`, with Γ being any type that is partially ordered and R being any type with a zero element, `x` is equal to `y` if and only if the coefficient functions of `x` and `y` are equal. In other words, two Hahn series are considered equal if they have the same coefficients for all indices.
More concisely: For any Hahn series x and y over the same index type and coefficient type, x = y if and only if the coefficient functions of x and y are equal.
|
HahnSeries.single_coeff_of_ne
theorem HahnSeries.single_coeff_of_ne :
∀ {Γ : Type u_1} {R : Type u_2} [inst : PartialOrder Γ] [inst_1 : Zero R] {a b : Γ} {r : R},
b ≠ a → ((HahnSeries.single a) r).coeff b = 0
The theorem `HahnSeries.single_coeff_of_ne` states that for any two distinct elements `a` and `b` of a partially ordered set `Γ` and any element `r` of a ring `R` with zero, the coefficient of `b` in the Hahn series obtained by assigning the coefficient `r` to `a` and zero to all other elements of `Γ` is zero. In other words, if `b` is not equal to `a`, the `b` coefficient of the Hahn series that has `r` at `a` and zero elsewhere is zero.
More concisely: For any distinct elements `a, b` in a partially ordered set `Γ` and any ring `R` with zero, the coefficient of `b` in the Hahn series assigning `r` to `a` and zero to other elements is zero.
|
HahnSeries.isPWO_support
theorem HahnSeries.isPWO_support :
∀ {Γ : Type u_1} {R : Type u_2} [inst : PartialOrder Γ] [inst_1 : Zero R] (x : HahnSeries Γ R), x.support.IsPWO
The theorem `HahnSeries.isPWO_support` states that for any Hahn Series `x`, with order type `Γ` and coefficient type `R`, where `Γ` is a partially ordered set and `R` is a type with a zero element, the support of `x` is a partially well-ordered set. In more detail, the support of a Hahn series is the set of indices whose coefficients are nonzero, and this theorem asserts that any infinite sequence in this support set contains a monotone subsequence of length 2 or an infinite monotone subsequence, which is the definition of a set being partially well-ordered.
More concisely: The support of a Hahn Series with order type Γ and coefficient type R, where Γ is a partially ordered set and R has a zero element, contains an infinite monotone subsequence.
|
HahnSeries.ext
theorem HahnSeries.ext :
∀ {Γ : Type u_1} {R : Type u_2} {inst : PartialOrder Γ} {inst_1 : Zero R} (x y : HahnSeries Γ R),
x.coeff = y.coeff → x = y
This theorem states that for any given types `Γ` and `R` where `Γ` is a partially ordered set and `R` is a ring with zero, if we have two Hahn series `x` and `y` (derived from `Γ` and `R`), then `x` equals `y` if and only if their coefficient functions are equal. Essentially, it states that Hahn series are completely determined by their coefficient functions.
More concisely: For any partially ordered sets Γ and rings with zero R, two Hahn series x and y over Γ and R are equal if and only if their coefficient functions coincide.
|
HahnSeries.embDomain_notin_image_support
theorem HahnSeries.embDomain_notin_image_support :
∀ {Γ : Type u_1} {R : Type u_2} [inst : PartialOrder Γ] [inst_1 : Zero R] {Γ' : Type u_3} [inst_2 : PartialOrder Γ']
{f : Γ ↪o Γ'} {x : HahnSeries Γ R} {b : Γ'}, b ∉ ⇑f '' x.support → (HahnSeries.embDomain f x).coeff b = 0
This theorem states that for any types `Γ` and `Γ'` with a partial order, type `R` with a zero element, an order-embedding `f` from `Γ` to `Γ'`, a Hahn series `x` over `Γ` with coefficients in `R`, and an element `b` of `Γ'`, if `b` is not in the image of the support of `x` under `f`, then the coefficient of `b` in the Hahn series obtained by extending the domain of `x` using `f` is zero.
In other words, when we extend the domain of a Hahn series, the new series will have zero coefficients at all indices that are not the image of the support of the original series.
More concisely: If `f` is an order-embedding from partially ordered types `Γ` to `Γ'`, `x` is a Hahn series over `Γ` with coefficients in a type `R` with zero element, and `b` is not in the image of the support of `x` under `f`, then the coefficient of `b` in the extended Hahn series of `x` is zero.
|
HahnSeries.support_nonempty_iff
theorem HahnSeries.support_nonempty_iff :
∀ {Γ : Type u_1} {R : Type u_2} [inst : PartialOrder Γ] [inst_1 : Zero R] {x : HahnSeries Γ R},
x.support.Nonempty ↔ x ≠ 0
The theorem `HahnSeries.support_nonempty_iff` states that for any given type `Γ` which has a partial order, any given type `R` which has a zero element, and any `HahnSeries` `x` of type `Γ` and `R`, the support set of `x` (i.e., the set of indices at which `x` has non-zero coefficients) is non-empty if and only if `x` is not equal to zero. In other words, a Hahn series is non-zero if and only if it has at least one non-zero coefficient.
More concisely: A Hahn series over a type with a partial order and a zero element is non-zero if and only if its support set is non-empty.
|
HahnSeries.isWF_support
theorem HahnSeries.isWF_support :
∀ {Γ : Type u_1} {R : Type u_2} [inst : PartialOrder Γ] [inst_1 : Zero R] (x : HahnSeries Γ R), x.support.IsWF := by
sorry
The theorem `HahnSeries.isWF_support` states that for all Hahn series (denoted by `x`), of a type `Γ` with a partial order and a type `R` with zero, the support of the Hahn series is well-founded. In other words, the set of indices in `Γ` whose coefficients in the Hahn series are non-zero (i.e., the support of the Hahn series) has a well-founded order using the `<` operation. Here, a set being well-founded means there are no infinite descending sequences.
More concisely: The support of a Hahn series over a well-ordered index set with respect to the partial order is a well-founded set.
|