Subfield.mem_iSup_of_directed
theorem Subfield.mem_iSup_of_directed :
∀ {K : Type u} [inst : DivisionRing K] {ι : Sort u_1} [hι : Nonempty ι] {S : ι → Subfield K},
Directed (fun x x_1 => x ≤ x_1) S → ∀ {x : K}, x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i
The theorem `Subfield.mem_iSup_of_directed` states that for any Division Ring `K`, any nonempty type `ι`, and any directed family of subfields `S : ι → Subfield K` (where the directedness is with respect to the subset relation), an element `x` of `K` is in the supremum of the subfields (i.e., the `sSup`, or smallest superset containing all subfields in the family) if and only if there exists an `i` in `ι` such that `x` is in the subfield `S i`. Note that this theorem would fail without the directedness assumption, as the union of two subfields is typically not a subfield.
More concisely: For any directed family of subfields of a division ring, an element is in their supremum if and only if it lies in one of the subfields.
|
Subfield.sub_mem
theorem Subfield.sub_mem :
∀ {K : Type u} [inst : DivisionRing K] (s : Subfield K) {x y : K}, x ∈ s → y ∈ s → x - y ∈ s
This theorem states that for any division ring `K` and any subfield `s` of `K`, if `x` and `y` are elements of `s`, then their difference `x - y` is also an element of `s`. In other words, the operation of subtraction is closed in the subfield `s`.
More concisely: For any subfield `s` of a division ring `K`, the subtraction operation on `s` is closed. That is, for all `x, y ∈ s`, we have `x - y ∈ s`.
|
Subfield.div_mem
theorem Subfield.div_mem :
∀ {K : Type u} [inst : DivisionRing K] (s : Subfield K) {x y : K}, x ∈ s → y ∈ s → x / y ∈ s
This theorem states that for any division ring `K`, and for any subfield `s` of `K`, if `x` and `y` are elements of `s`, then the result of the division of `x` by `y` (denoted as `x / y`) is also an element of `s`. Essentially, it asserts that a subfield is closed under the operation of division. This means that dividing any two elements of the subfield always results in a value that is also in the subfield.
More concisely: If `s` is a subfield of the division ring `K`, then for all `x, y ∈ s`, `x / y ∈ s`.
|
Subfield.one_mem
theorem Subfield.one_mem : ∀ {K : Type u} [inst : DivisionRing K] (s : Subfield K), 1 ∈ s
This theorem states that for any division ring `K` and any subfield `s` of `K`, the multiplicative identity, 1, is an element of `s`. In other words, every subfield of a division ring must contain the number 1.
More concisely: Every subfield of a division ring contains the multiplicative identity 1.
|
Subfield.closure_mono
theorem Subfield.closure_mono :
∀ {K : Type u} [inst : DivisionRing K] ⦃s t : Set K⦄, s ⊆ t → Subfield.closure s ≤ Subfield.closure t
The theorem `Subfield.closure_mono` states that the closure operation of a subfield over a set is monotone with respect to the set. This means that for any given division ring `K` and any two sets `s` and `t` of elements from `K`, if set `s` is a subset of set `t` (denoted as `s ⊆ t`), then the subfield generated by `s` is a subfield of (or equal to) the subfield generated by `t` (`Subfield.closure s ≤ Subfield.closure t`). In other words, increasing the set of elements in a division ring will not decrease the corresponding generated subfield.
More concisely: The subfield generation operation is monotone with respect to set inclusion. That is, for any division ring K and sets s ⊆ t of its elements, the subfield generated by s is included in (or equal to) the subfield generated by t.
|
Subfield.list_prod_mem
theorem Subfield.list_prod_mem :
∀ {K : Type u} [inst : DivisionRing K] (s : Subfield K) {l : List K}, (∀ x ∈ l, x ∈ s) → l.prod ∈ s
This theorem states that the product of a list of elements in a subfield is also in the subfield. In other words, if you have a list of elements from a subfield of a division ring, the product of all elements in this list is an element of the same subfield. This applies to any division ring `K` and any subfield `s` of `K`.
More concisely: If `s` is a subfield of the division ring `K`, then the product of any finite list of elements in `s` belongs to `s`.
|
Subfield.multiset_sum_mem
theorem Subfield.multiset_sum_mem :
∀ {K : Type u} [inst : DivisionRing K] (s : Subfield K) (m : Multiset K), (∀ a ∈ m, a ∈ s) → m.sum ∈ s
The theorem `Subfield.multiset_sum_mem` states that for any type `K` that has a `DivisionRing` structure, and any `Subfield` of `K` denoted `s`, and any multiset `m` whose elements are of type `K`, if each element `a` in `m` is also an element of the `Subfield` `s`, then the sum of all elements in the multiset `m` is also in the `Subfield` `s`. Essentially, it's stating that the sum of a multiset of elements from a specific subfield remains in that subfield.
More concisely: If `s` is a subfield of a division ring `K` and all elements in the multiset `m` over `K` belong to `s`, then the sum of `m` belongs to `s`.
|
Subfield.subset_closure
theorem Subfield.subset_closure : ∀ {K : Type u} [inst : DivisionRing K] {s : Set K}, s ⊆ ↑(Subfield.closure s) := by
sorry
This theorem asserts that for any given type `K` equipped with a division ring structure and any set `s` of elements from `K`, the set `s` is included in or is a subset of the subfield generated by `s`. In other words, all elements in the initial set `s` are also present in the subfield that is constructed from `s`. This is a fundamental property of closure operations in algebraic structures like fields and rings.
More concisely: For any division ring `K` and set `s` of elements from `K`, the subfield generated by `s` contains `s`.
|
Subfield.closure_eq
theorem Subfield.closure_eq : ∀ {K : Type u} [inst : DivisionRing K] (s : Subfield K), Subfield.closure ↑s = s := by
sorry
The theorem states that for any type `K` which is a division ring, the closure of a subfield `s` of `K` is equal to the subfield `s` itself. Here, the closure of a subfield `s` is defined as the smallest subfield that contains all elements of `s`. This theorem thus essentially says that the smallest subfield containing all elements of a given subfield `s` is `s` itself.
More concisely: For any subfield `s` of a division ring `K`, the subfield generated by `s` is equal to `s` itself.
|
Subfield.closure_le
theorem Subfield.closure_le :
∀ {K : Type u} [inst : DivisionRing K] {s : Set K} {t : Subfield K}, Subfield.closure s ≤ t ↔ s ⊆ ↑t
This theorem states that for any type `K` equipped with a `DivisionRing` structure, and any set `s` of type `K` and subfield `t` of type `K`, the closure of the set `s` under the operation of the subfield is a subset of `t` if and only if `s` is a subset of `t`. In other words, a subfield `t` contains the closure of a set `s` exactly when it contains the set `s` itself. This encapsulates the idea of a closure operation, which gathers all elements related to the set `s` under the operations of the subfield in a way that the result is still within the subfield `t`.
More concisely: For any set `s` and subfield `t` of a division ring `K`, the closure of `s` under `t` equals `s` if and only if `s` is a subset of `t`.
|
Subfield.add_mem
theorem Subfield.add_mem :
∀ {K : Type u} [inst : DivisionRing K] (s : Subfield K) {x y : K}, x ∈ s → y ∈ s → x + y ∈ s
This theorem states that a subfield is closed under addition. Specifically, given any type `K` that has a division ring structure, for any subfield `s` of `K`, and any two elements `x` and `y` from `K`, if `x` and `y` are members of the subfield `s`, then their sum `x + y` is also a member of the subfield `s`. This is a fundamental property of subfields in the field of mathematics.
More concisely: Given a subfield `s` of a division ring `K`, if `x, y` belong to `s`, then `x + y` also belongs to `s`.
|
Subfield.ext
theorem Subfield.ext : ∀ {K : Type u} [inst : DivisionRing K] {S T : Subfield K}, (∀ (x : K), x ∈ S ↔ x ∈ T) → S = T
The theorem `Subfield.ext` states that for any type `K` that has a `DivisionRing` structure, if we have two subfields `S` and `T` of `K`, and every element `x` of `K` is in `S` if and only if it is in `T`, then `S` and `T` must be the same subfield. In other words, two subfields of a division ring are considered equal if they contain exactly the same elements.
More concisely: If two subfields of a division ring have the same elements, then they are equal.
|
Subfield.coe_sInf
theorem Subfield.coe_sInf : ∀ {K : Type u} [inst : DivisionRing K] (S : Set (Subfield K)), ↑(sInf S) = ⋂ s ∈ S, ↑s := by
sorry
This theorem states that for any division ring `K` and any set `S` of subfields of `K`, the set of elements of the greatest lower bound (`sInf`) of `S` is equal to the intersection of the set of elements of all subfields in `S`. In other words, each element of the greatest lower bound subfield must be an element in all subfields in `S`. This theorem provides the condition for an element to be in the greatest lower bound of a set of subfields.
More concisely: The greatest lower bound of a set `S` of subfields of a division ring `K` is the intersection of all subfields in `S`.
|
RingHom.eqOn_field_closure
theorem RingHom.eqOn_field_closure :
∀ {K : Type u} [inst : DivisionRing K] {L : Type v} [inst_1 : Semiring L] {f g : K →+* L} {s : Set K},
Set.EqOn (⇑f) (⇑g) s → Set.EqOn ⇑f ⇑g ↑(Subfield.closure s)
This theorem, `RingHom.eqOn_field_closure`, states that for any division ring `K` and semiring `L`, if two ring homomorphisms `f` and `g` from `K` to `L` are equal on a set `s` (i.e., they map any element `x` in `s` to the same element in `L`), then they are also equal on the subfield closure of `s`. In other words, the equality of two ring homomorphisms on a set extends to the equality on the smallest subfield of `K` that contains this set.
More concisely: If two ring homomorphisms from a division ring to a semiring agree on a set, they agree on the subfield closure of that set.
|
Subfield.prod_mem
theorem Subfield.prod_mem :
∀ {K : Type u} [inst : Field K] (s : Subfield K) {ι : Type u_1} {t : Finset ι} {f : ι → K},
(∀ c ∈ t, f c ∈ s) → (t.prod fun i => f i) ∈ s
This theorem states that, for any type `K` with a `Field` structure, any subfield `s` of `K`, a `Finset` `t` indexed by an arbitrary type `ι`, and a function `f` mapping `ι` to `K`, if every element `c` in `t` maps to an element in the subfield `s` under the function `f`, then the product of the elements in `t` under the function `f` is also in the subfield `s`. In other words, the product of the elements of a subfield, indexed by a finite set, is itself an element of the subfield.
More concisely: For any field `K`, subfield `s`, Finset `t` indexed by an arbitrary type `ι`, and function `f` from `ι` to `K` such that `f(c) ∈ s` for all `c ∈ t`, the product of `f(i)` for all `i ∈ t` is in `s`.
|
Subfield.zero_mem
theorem Subfield.zero_mem : ∀ {K : Type u} [inst : DivisionRing K] (s : Subfield K), 0 ∈ s
This theorem states that for any given division ring `K` and any subfield `s` of `K`, the element `0` (zero) from `K` is also an element in `s`. In other words, every subfield of a division ring must contain the zero of the division ring.
More concisely: Every subfield of a division ring contains its additive identity (zero).
|
Subfield.sum_mem
theorem Subfield.sum_mem :
∀ {K : Type u} [inst : DivisionRing K] (s : Subfield K) {ι : Type u_1} {t : Finset ι} {f : ι → K},
(∀ c ∈ t, f c ∈ s) → (t.sum fun i => f i) ∈ s
This theorem states that the sum of elements in a `Subfield` of a `DivisionRing`, indexed by a `Finset`, is also in the `Subfield`. More specifically, given a `DivisionRing` K, a `Subfield` s of K, a `Finset` t, and a function f mapping elements of the finset to K, if every element mapped by f is in the subfield s, then the sum of all these elements (as given by the sum of f over t) is also in s.
More concisely: Given a Division Ring K, a Subfield s of K, a Finset t, and a function f: t → K with all images in s, the sum ∑ x in t, f(x) is in s.
|
Subfield.gc_map_comap
theorem Subfield.gc_map_comap :
∀ {K : Type u} {L : Type v} [inst : DivisionRing K] [inst_1 : DivisionRing L] (f : K →+* L),
GaloisConnection (Subfield.map f) (Subfield.comap f)
The theorem `Subfield.gc_map_comap` states that for any division rings `K` and `L`, and any ring homomorphism `f` from `K` to `L`, there exists a Galois connection between the mapping of a subfield along `f` and the preimage of a subfield along `f`. In other words, for any subfield `a` of `K` and subfield `b` of `L`, `a` is mapped to a subfield that's less than or equal to `b` through `f` if and only if `a` is less than or equal to the preimage of `b` through `f`. This connects the concepts of subfield mapping and preimage, and shows that they form a Galois connection, a special case of adjoint functors in category theory.
More concisely: For any division rings K and L and ring homomorphism f from K to L, the mapping of subfields of K along f and the preimage of subfields of L along f form a Galois connection.
|
Subfield.closure_induction
theorem Subfield.closure_induction :
∀ {K : Type u} [inst : DivisionRing K] {s : Set K} {p : K → Prop} {x : K},
x ∈ Subfield.closure s →
(∀ x ∈ s, p x) →
p 1 →
(∀ (x y : K), p x → p y → p (x + y)) →
(∀ (x : K), p x → p (-x)) → (∀ (x : K), p x → p x⁻¹) → (∀ (x y : K), p x → p y → p (x * y)) → p x
This theorem provides an induction principle for closure membership. In a given division ring `K` and for a set `s` of elements of `K`, the theorem states that if a property `p` holds for `1`, all elements of `s`, and is preserved under operations of addition, negation, multiplication, and inversion, then this property `p` also holds for all elements contained within the closure of `s` in `K`. The closure of `s`, denoted as `Subfield.closure s`, is the smallest subfield of `K` that includes all elements of `s`.
In other words, if a property is true for all elements in a certain set and some special element (here it is `1`), and this property is maintained when applying addition, negation, multiplication, and inversion operations, then this property can be extended to hold for all elements in the closure of the initial set.
More concisely: If a property holds for all elements of a set `s` and 1 in a division ring `K`, and is closed under addition, negation, multiplication, and inversion, then the property holds for all elements in the subfield closure of `s` in `K`.
|
Subfield.neg_mem
theorem Subfield.neg_mem : ∀ {K : Type u} [inst : DivisionRing K] (s : Subfield K) {x : K}, x ∈ s → -x ∈ s
This theorem states that a subfield is closed under negation. In other words, for any division ring `K` and any subfield `s` of `K`, if a number `x` is in `s`, then its negation `-x` is also in `s`. This is a fundamental property of subfields in the context of algebra.
More concisely: If `s` is a subfield of the division ring `K`, then for all `x` in `s`, the negation `-x` is also in `s`.
|
RingHom.map_field_closure
theorem RingHom.map_field_closure :
∀ {K : Type u} {L : Type v} [inst : DivisionRing K] [inst_1 : DivisionRing L] (f : K →+* L) (s : Set K),
Subfield.map f (Subfield.closure s) = Subfield.closure (⇑f '' s)
This theorem states that for any two types `K` and `L` that are division rings, and any ring homomorphism `f` from `K` to `L`, if you generate a subfield from a set `s` in `K` and map it to `L` using `f`, the result is the same as if you first apply the homomorphism `f` to the set `s` and then generate the subfield in `L`. In mathematical terms, the image under a ring homomorphism of the subfield generated by a set is equal to the subfield generated by the image of the set.
More concisely: For any division rings K and L and ring homomorphism f from K to L, the subfield generated by the image of a subset in K under f is equal to the image of the subfield generated by that subset in K.
|
Subfield.mul_mem
theorem Subfield.mul_mem :
∀ {K : Type u} [inst : DivisionRing K] (s : Subfield K) {x y : K}, x ∈ s → y ∈ s → x * y ∈ s
This theorem states that a subfield in a division ring is closed under multiplication. In more detail, for any division ring 'K', given any subfield 's' of 'K', and any two elements 'x' and 'y' in 's', the product of 'x' and 'y' is also an element of 's'. In essence, this means you can multiply any two elements in the subfield and the result will still belong to the same subfield, hence demonstrating the closure property in the context of multiplication.
More concisely: In any division ring 'K' and subfield 's', for all elements 'x' and 'y' in 's', the product 'x' * 'y' lies in 's'.
|
Subfield.multiset_prod_mem
theorem Subfield.multiset_prod_mem :
∀ {K : Type u} [inst : Field K] (s : Subfield K) (m : Multiset K), (∀ a ∈ m, a ∈ s) → m.prod ∈ s
This theorem states that for any given type `K` which is a field, a subfield `s` of `K`, and a multiset `m` of elements from `K`, if every element `a` from the multiset `m` belongs to the subfield `s`, then the product of all elements in the multiset `m` also belongs to the subfield `s`. In mathematical notation this can be represented as: for every multiset $m$ of elements $a$ from a subfield $s$ of a field $K$, if $a \in s$ for all $a \in m$, then $\prod m \in s$.
More concisely: If every element in a multiset of a subfield of a field belongs to the subfield, then their product belongs to the subfield.
|
Subfield.inv_mem
theorem Subfield.inv_mem : ∀ {K : Type u} [inst : DivisionRing K] (s : Subfield K) {x : K}, x ∈ s → x⁻¹ ∈ s
This theorem states that a subfield is closed under the operation of taking inverses. Specifically, for any type 'K' that has a structure of a division ring, any subfield 's' of 'K', and any element 'x' of 'K', if 'x' is in 's', then the inverse of 'x' is also in 's'.
More concisely: In a division ring 'K', the subfield 's' is closed under taking inverses, i.e., if 'x' is an element of 's', then the multiplicative inverse of 'x' is also an element of 's'.
|
Subfield.list_sum_mem
theorem Subfield.list_sum_mem :
∀ {K : Type u} [inst : DivisionRing K] (s : Subfield K) {l : List K}, (∀ x ∈ l, x ∈ s) → l.sum ∈ s
This theorem states that for any type `K` that has a `DivisionRing` structure, if we have a `Subfield` `s` of `K` and a list `l` of elements from `K`, then if every element `x` of `l` belongs to `s`, the sum of all elements in `l` also belongs to `s`. In mathematical terms, it asserts that the sum of elements in a subfield is also an element of the subfield.
More concisely: If `s` is a subfield of a division ring `K`, then the sum of any list of elements in `s` belongs to `s`.
|
Subfield.inv_mem'
theorem Subfield.inv_mem' :
∀ {K : Type u} [inst : DivisionRing K] (self : Subfield K), ∀ x ∈ self.carrier, x⁻¹ ∈ self.carrier
This theorem states that in any given division ring `K`, for each element `x` of a subfield `self` of `K`, the multiplicative inverse of `x` (denoted as `x⁻¹`) is also a member of the same subfield. In other words, the set of all elements of a subfield is closed under the operation of taking multiplicative inverses. This is a property of subfields in the context of division rings.
More concisely: In any division ring, the multiplicative inverses of elements in a subfield belong to the same subfield.
|