IntermediateField.eq_of_le_of_finrank_le
theorem IntermediateField.eq_of_le_of_finrank_le :
∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
{F E : IntermediateField K L} [hfin : FiniteDimensional K ↥E],
F ≤ E → FiniteDimensional.finrank K ↥E ≤ FiniteDimensional.finrank K ↥F → F = E
This theorem states that if `F` and `E` are two intermediate fields of a field extension `L / K` such that the dimension of `E` over `K` is less than or equal to the dimension of `F` over `K` (denoted as `[E : K] ≤ [F : K]`), and both of these dimensions are finite, then `F` is equal to `E`. This essentially says that if two intermediate fields of a field extension have the same finite dimension over the base field, they must be the same field.
More concisely: If `F` and `E` are intermediate fields of a finite field extension `L/K` with `[E : K] ≤ [F : K]`, then `F = E`.
|
IntermediateField.multiset_prod_mem
theorem IntermediateField.multiset_prod_mem :
∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
(S : IntermediateField K L) (m : Multiset L), (∀ a ∈ m, a ∈ S) → m.prod ∈ S
The theorem `IntermediateField.multiset_prod_mem` states that for any two types `K` and `L`, where `K` and `L` are fields and `L` is an algebra over `K`, if there is an intermediate field `S` between `K` and `L` and a multiset `m` of elements from `L`, then the product of all elements of `m` is in `S` if every element of `m` is in `S`. In other words, if every element of a multiset is in an intermediate field, then the product of the multiset's elements is also in that intermediate field.
More concisely: If `K` and `L` are fields with `L` an algebra over `K`, and there is an intermediate field `S` between `K` and `L`, then for any multiset `m` of elements from `L` all in `S`, the product of `m` is in `S`.
|
IntermediateField.algebraMap_mem
theorem IntermediateField.algebraMap_mem :
∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
(S : IntermediateField K L) (x : K), (algebraMap K L) x ∈ S
This theorem states that for any two fields `K` and `L` where `K` is an algebra over `L`, and for any intermediate field `S` between `K` and `L`, the image of any element `x` of `K` under the algebra map from `K` to `L` is always an element of the intermediate field `S`. In other words, the intermediate field `S` contains the image of the smaller field `K` under the algebra map.
More concisely: For any fields K being a subalgebra over L, and any intermediate field S between K and L, the image of any element x in K under the algebra map from K to L lies in the intermediate field S.
|
IntermediateField.eq_of_le_of_finrank_eq
theorem IntermediateField.eq_of_le_of_finrank_eq :
∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
{F E : IntermediateField K L} [inst_3 : FiniteDimensional K ↥E],
F ≤ E → FiniteDimensional.finrank K ↥F = FiniteDimensional.finrank K ↥E → F = E
The theorem `IntermediateField.eq_of_le_of_finrank_eq` states that given two intermediate fields `F` and `E` of a field extension `L / K`, if `F` is contained in or equal to `E` (denoted as `F ≤ E`) and they both have the same finite dimension over the base field `K` (expressed as `[F : K] = [E : K]`), then `F` must be equal to `E`.
More concisely: If intermediate fields $F$ and $E$ of a field extension $L/K$ satisfy $F \leq E$ and $[F:K] = [E:K]$, then $F = E$.
|
IntermediateField.fieldRange_val
theorem IntermediateField.fieldRange_val :
∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
(S : IntermediateField K L), S.val.fieldRange = S
The theorem `IntermediateField.fieldRange_val` states that for any field `K`, any field `L` that is an algebra over `K`, and any intermediate field `S` of `L / K`, the range of the algebra homomorphism that embeds the elements of `S` into `L` (as obtained by the function `IntermediateField.val`) is `S` itself. In mathematical terms, if `S` is an intermediate field of `K` and `L`, then the image of `S` under the canonical embedding into `L` is precisely `S`.
More concisely: The theorem asserts that the image of an intermediate field under the canonical embedding into a larger field is equal to the field itself.
|
IntermediateField.sum_mem
theorem IntermediateField.sum_mem :
∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
(S : IntermediateField K L) {ι : Type u_4} {t : Finset ι} {f : ι → L},
(∀ c ∈ t, f c ∈ S) → (t.sum fun i => f i) ∈ S
This theorem states that for any intermediate field `S` between fields `K` and `L` with `K` and `L` being fields, and `K` being an algebra over `L`, the sum of any finite set of elements (expressed as a `Finset`) from field `L`, with each element also belonging to the intermediate field `S`, also belongs to the intermediate field `S`. In other words, the sum of any number of elements from an intermediate field is also in the intermediate field.
More concisely: For any intermediate field `S` between fields `K` and `L` with `K` being an algebra over `L`, the sum of any finite set of elements from `L` that lie in `S` also lies in `S`.
|
IntermediateField.sub_mem
theorem IntermediateField.sub_mem :
∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
(S : IntermediateField K L) {x y : L}, x ∈ S → y ∈ S → x - y ∈ S
This theorem states that for any intermediate field `S` between two fields `K` and `L`, given any two elements `x` and `y` from the field `L` that are also in `S`, their difference (`x - y`) is also an element of the intermediate field `S`. Here, `K` and `L` are fields with `L` being an algebra over `K`. This shows that an intermediate field is closed under the operation of subtraction.
More concisely: For any fields $K \subseteq S \subseteq L$, and any $x, y \in L$ that are also in $S$, $x - y \in S$.
|
IntermediateField.mul_mem
theorem IntermediateField.mul_mem :
∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
(S : IntermediateField K L) {x y : L}, x ∈ S → y ∈ S → x * y ∈ S
This theorem states that an intermediate field is closed under multiplication. Specifically, for any two elements 'x' and 'y' from an intermediate field 'S' between two fields 'K' and 'L', where 'K' and 'L' are fields and 'K' is an algebra over 'L', if 'x' and 'y' are elements of 'S', then their product 'x * y' is also an element of 'S'. Therefore, multiplication within an intermediate field remains within that field.
More concisely: An intermediate field between two fields, being a subring of the containing field, is closed under multiplication.
|
IntermediateField.zero_mem
theorem IntermediateField.zero_mem :
∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
(S : IntermediateField K L), 0 ∈ S
This theorem states that, for any intermediate field `S` between two fields `K` and `L`, the element `0` of the ring is always contained in `S`. Here, `K` and `L` are arbitrary types representing fields, and the `Algebra K L` instance indicates that `L` is an algebra over `K`. An intermediate field `S` is a subfield of `L` that contains `K`.
More concisely: For any field extension `L` being an algebra over a base field `K`, and any intermediate field `S` between `K` and `L`, the element `0` of `K` belongs to `S`.
|
IntermediateField.map_le_iff_le_comap
theorem IntermediateField.map_le_iff_le_comap :
∀ {K : Type u_1} {L : Type u_2} {L' : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Field L']
[inst_3 : Algebra K L] [inst_4 : Algebra K L'] {f : L →ₐ[K] L'} {s : IntermediateField K L}
{t : IntermediateField K L'}, IntermediateField.map f s ≤ t ↔ s ≤ IntermediateField.comap f t
The theorem `IntermediateField.map_le_iff_le_comap` states that for any fields `K`, `L` and `L'`, with `L` and `L'` being extensions of `K`, any `K`-algebra homomorphism `f` from `L` to `L'`, and any intermediate fields `s` in `L` and `t` in `L'`, the image of `s` under `f` is a subset of `t` if and only if `s` is a subset of the preimage of `t` under `f`. In other words, this theorem describes a relationship between intermediate fields under a homomorphism and its inverse operation.
More concisely: For any fields K, L, L', homomorphism f from L to L', and intermediate fields s in L and t in L', the image of s under f is a subset of t if and only if s is a subset of the preimage of t under f.
|
IntermediateField.ext
theorem IntermediateField.ext :
∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
{S T : IntermediateField K L}, (∀ (x : L), x ∈ S ↔ x ∈ T) → S = T
This theorem states that for any two intermediate fields `S` and `T` of a field extension `L/K`, if every element `x` of the extension `L` is in `S` if and only if it is in `T`, then `S` is equal to `T`. Here, `K` and `L` are fields and `L` is an algebra over `K`, which means that `L` can be viewed as a vector space over `K`. The theorem thus captures the intuition that two sets are equal if they have exactly the same elements, specialized to the case of intermediate fields in a field extension.
More concisely: If two intermediate fields `S` and `T` of a field extension `L/K` have equal elements, then `S` equals `T`.
|
IntermediateField.toSubalgebra_injective
theorem IntermediateField.toSubalgebra_injective :
∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L],
Function.Injective IntermediateField.toSubalgebra
The theorem `IntermediateField.toSubalgebra_injective` states that for any types `K` and `L` that are fields with `K` being an algebra over `L`, the function `IntermediateField.toSubalgebra`, which reinterprets an `IntermediateField` as a `Subalgebra`, is injective. This means that if two different intermediate fields of `K` over `L` are transformed into the same subalgebra via `IntermediateField.toSubalgebra`, they must have originally been the same intermediate field. In essence, no information is lost when converting from an `IntermediateField` to a `Subalgebra`.
More concisely: The function `IntermediateField.toSubalgebra` maps distinct intermediate fields of `K` over `L` to distinct subalgebras.
|
IntermediateField.multiset_sum_mem
theorem IntermediateField.multiset_sum_mem :
∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
(S : IntermediateField K L) (m : Multiset L), (∀ a ∈ m, a ∈ S) → m.sum ∈ S
The theorem `IntermediateField.multiset_sum_mem` states that for any types `K` and `L` which are fields and for any `K`-algebra structure on `L`, given an `IntermediateField` `S` of `K` and `L`, and a multiset `m` of elements from `L`, if every element `a` of the multiset `m` belongs to `S`, then the sum of the elements in multiset `m` is also in `S`. Essentially, this theorem is asserting that the sum of a collection of elements in an intermediate field remains in that intermediate field.
More concisely: Given a field extension `S` of fields `K` and `L`, if every element in the multiset `m` of `L` belongs to `S`, then the sum of the elements in `m` is also in `S`.
|
IntermediateField.eq_of_le_of_finrank_eq'
theorem IntermediateField.eq_of_le_of_finrank_eq' :
∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
{F E : IntermediateField K L} [inst_3 : FiniteDimensional (↥F) L],
F ≤ E → FiniteDimensional.finrank (↥F) L = FiniteDimensional.finrank (↥E) L → F = E
This theorem asserts that if `F` and `E` are two intermediate fields of a field extension `L / K`, and if both `F` and `E` have the same finite dimension over `L` (that is, `[L : F]` and `[L : E]` are equal), then `F` must be equal to `E`. The equality is predicated on the condition that `F` is a subspace of `E`. This is essentially a statement about the uniqueness of subspaces of a given dimension in a vector space, applied to the particular case of field extensions.
More concisely: If two intermediate fields `F` and `E` of a field extension `L / K` have the same finite dimension over `L` (i.e., `[L : F] = [L : E]`) and `F` is a subspace of `E`, then `F` equals `E`.
|
IntermediateField.list_prod_mem
theorem IntermediateField.list_prod_mem :
∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
(S : IntermediateField K L) {l : List L}, (∀ x ∈ l, x ∈ S) → l.prod ∈ S
This theorem asserts that for any given list of elements from an algebraic structure `L`, if each of these elements belongs to an intermediate field `S` (which is an intermediate field between a field `K` and another algebraic structure `L`), then the product of all elements in the list also belongs to this intermediate field `S`. This applies to any types `K` and `L` where `K` is a field, `L` is another field, and there's a specified algebra between `K` and `L`.
More concisely: For any list of elements from fields `L` that lie in an intermediate field `S` between fields `K` and `L`, the product of these elements also belongs to `S`.
|
IntermediateField.prod_mem
theorem IntermediateField.prod_mem :
∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
(S : IntermediateField K L) {ι : Type u_4} {t : Finset ι} {f : ι → L},
(∀ c ∈ t, f c ∈ S) → (t.prod fun i => f i) ∈ S
This theorem states that for any given fields K and L, an intermediate field S between K and L, a finite set 't' of some type ι, and a function 'f' mapping elements of ι to elements of L, if every value of 'f' for elements in 't' belongs to the intermediate field S, then the product of those function values also belongs to the intermediate field S. This theorem asserts the closure property of intermediate fields with respect to the multiplication operation on the elements of a finite set which are mapped to the intermediate field.
More concisely: If fields K ⊆ S ⊆ L, t is a finite set, and f : ι → L with image(f)(t) ⊆ S, then f(ι) ⊆ S implies prod(map f t) ∈ S. (Here, ι is some type, map is the function space, and prod denotes the product of elements.)
|
IntermediateField.add_mem
theorem IntermediateField.add_mem :
∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
(S : IntermediateField K L) {x y : L}, x ∈ S → y ∈ S → x + y ∈ S
This theorem states that an intermediate field, represented as `S`, is closed under addition. Specifically, for any two elements `x` and `y` from a field extension `L` of a field `K`, if both `x` and `y` are elements of the intermediate field `S`, then their sum `x + y` is also an element of `S`. This closure property is a fundamental characteristic of fields in the context of abstract algebra.
More concisely: If `S` is an intermediate field of a field extension `L/K`, then for all `x, y ∈ S`, we have `x + y ∈ S`.
|
IntermediateField.list_sum_mem
theorem IntermediateField.list_sum_mem :
∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
(S : IntermediateField K L) {l : List L}, (∀ x ∈ l, x ∈ S) → l.sum ∈ S
This theorem states that for any two types `K` and `L` that are fields with an algebra structure between them, and any intermediate field `S` between `K` and `L`, if every element `x` of a list `l` of type `L` is in the intermediate field `S`, then the sum of the elements of `l` is also in `S`. In mathematical terms, let `K` and `L` be fields with `K` ≤ `L` and `S` an intermediate field (`K` ≤ `S` ≤ `L`). Given a list of elements in `L`, if every element of the list is in `S`, then the sum of the list of elements is also in `S`.
More concisely: If `K` and `L` are fields with `K` ≤ `L`, `S` an intermediate field (`K` ≤ `S` ≤ `L`), and all elements of a list `l` in `L` belong to `S`, then the sum of `l` belongs to `S`.
|
IntermediateField.inv_mem
theorem IntermediateField.inv_mem :
∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
(S : IntermediateField K L) {x : L}, x ∈ S → x⁻¹ ∈ S
This theorem states that an intermediate field is closed under the operation of taking inverses. More specifically, for any fields `K` and `L` with `L` being an algebra over `K`, and `S` being an intermediate field between `K` and `L`, if an element `x` from `L` is in `S`, then the inverse of `x` (denoted `x⁻¹`) is also in `S`. This means that taking the inverse of any element in the intermediate field will yield another element that also belongs to the intermediate field.
More concisely: If `K` is a field, `L` is an algebra over `K`, `S` is an intermediate field between `K` and `L`, and `x` is an element of `L` in `S`, then `x⁻¹` is also in `S`.
|
IntermediateField.smul_mem
theorem IntermediateField.smul_mem :
∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
(S : IntermediateField K L) {y : L}, y ∈ S → ∀ {x : K}, x • y ∈ S
This theorem states that an intermediate field, represented by `S`, is closed under scalar multiplication. Specifically, it means that for any two given types `K` and `L` where `K` and `L` are fields and `K` is an algebra over `L`, if an element `y` from `L` is in the intermediate field `S`, then the result of scalar multiplication of `y` by any scalar `x` from `K` is also in `S`.
More concisely: If `S` is an intermediate field of a field extension `K/L`, then for all `y ∈ L` and `x ∈ K`, the scalar multiplication `xy` belongs to `S`.
|
IntermediateField.minpoly_eq
theorem IntermediateField.minpoly_eq :
∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
{S : IntermediateField K L} (x : ↥S), minpoly K x = minpoly K ↑x
The theorem `IntermediateField.minpoly_eq` states that for any fields `K` and `L` with algebra structure between them, and any intermediate field `S` between `K` and `L`, the minimal polynomial of an element `x` from `S` (considered as an element of `S`) is the same as the minimal polynomial of `x` considered as an element of the larger field `L` (i.e., `x` is coerced to `L`). The minimal polynomial is a key concept in field theory and algebra, which gives the polynomial with coefficients in `K` that `x` is a root of and no other polynomial with lower degree has `x` as a root.
More concisely: For any fields `K` and `L` with algebra structure between them and an intermediate field `S` between `K` and `L`, the minimal polynomial of an element `x` in `S` regarded as an element of both `S` and `L` is equal.
|
IntermediateField.div_mem
theorem IntermediateField.div_mem :
∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
(S : IntermediateField K L) {x y : L}, x ∈ S → y ∈ S → x / y ∈ S
This theorem states that an intermediate field, denoted by 'S', is closed under division. More specifically, for any two elements 'x' and 'y' of a field extension L of a field K (where L is a field and K is the base field), if 'x' and 'y' belong to the intermediate field 'S', then the result of the division of 'x' by 'y' also belongs to 'S'. In other words, the intermediate field 'S' retains the division property of the field.
More concisely: If $L/K$ is a field extension and $x, y \in S \subseteq L$ are elements of an intermediate field $S$, then $\frac{x}{y} \in S$.
|
IntermediateField.eq_of_le_of_finrank_le'
theorem IntermediateField.eq_of_le_of_finrank_le' :
∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
{F E : IntermediateField K L} [inst_3 : FiniteDimensional (↥F) L],
F ≤ E → FiniteDimensional.finrank (↥F) L ≤ FiniteDimensional.finrank (↥E) L → F = E
The theorem `IntermediateField.eq_of_le_of_finrank_le'` states that if `F` and `E` are two intermediate fields of a field extension `L / K`, and the rank of `L` over `F` is finite and less than or equal to the rank of `L` over `E` (denoted as `[L : F] ≤ [L : E]`), then `F` and `E` must be identical, i.e., `F = E`. In simpler terms, if we have two subsets `F` and `E` of a space `L`, and `F` is contained in `E` and both `F` and `E` have finite dimensions with the dimension of `F` being less than or equal to the dimension of `E`, then `F` and `E` are exactly the same.
More concisely: If `F` and `E` are intermediate fields of a field extension `L/K` with finite dimensions `[L:F]` and `[L:E]` satisfying `[L:F] ≤ [L:E]`, then `F = E`.
|
IntermediateField.one_mem
theorem IntermediateField.one_mem :
∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
(S : IntermediateField K L), 1 ∈ S
This theorem states that for any intermediate field `S` of two types `K` and `L` (which are fields themselves), the number one (1) is an element of the intermediate field `S`. This is true regardless of the specific fields `K` and `L` and the algebra structure defined over them.
More concisely: For any intermediate field `S` of two fields `K` and `L`, the multiplicative identity 1 belongs to `S`.
|