solvableByRad.induction3
theorem solvableByRad.induction3 :
∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E]
{α : ↥(solvableByRad F E)} {n : ℕ}, n ≠ 0 → solvableByRad.P (α ^ n) → solvableByRad.P α
This theorem, `solvableByRad.induction3`, states that for any fields `F` and `E` where `E` is an algebra over `F`, and for any element `α` in the intermediate field of `E` over `F` that is solvable by radicals, if `n` is a non-zero natural number and the `n`-th power of `α` satisfies the property `solvableByRad.P`, then `α` itself also satisfies `solvableByRad.P`. In simpler words, if the `n`-th power of `α` has a minimal polynomial whose Galois group is solvable, then the minimal polynomial of `α` itself also has a solvable Galois group.
More concisely: If `α` is a solvable-by-radicals element in an algebra `E` over a field `F`, and the minimal polynomial of `α`'s `n`-th power has a solvable Galois group, then the minimal polynomial of `α` itself has a solvable Galois group.
|
solvableByRad.isSolvable'
theorem solvableByRad.isSolvable' :
∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {α : E}
{q : Polynomial F}, Irreducible q → (Polynomial.aeval α) q = 0 → IsSolvableByRad F α → IsSolvable q.Gal
The **Abel-Ruffini Theorem** (in one direction) states that if we have an irreducible polynomial `q` over a field `F` and a root `α` in an algebra over `F`, given that `α` is solvable by radicals (denoted by `IsSolvableByRad F α`), and the polynomial `q` takes the value 0 when evaluated at `α` (denoted by `(Polynomial.aeval α) q = 0`), then the Galois group of the polynomial `q` is solvable (denoted by `IsSolvable q.Gal`).
In other words, if a polynomial with coefficients in a field can be factored into linear factors over an extension field, and one of its roots can be expressed using addition, multiplication, and radicals, then the Galois group of the polynomial is solvable. This theorem is one direction of the Abel-Ruffini theorem and is a significant result in the theory of solvability of polynomial equations.
More concisely: If an irreducible polynomial over a field has a root that is solvable by radicals, then its Galois group is solvable.
|
solvableByRad.induction2
theorem solvableByRad.induction2 :
∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E]
{α β γ : ↥(solvableByRad F E)}, γ ∈ F⟮α, β⟯ → solvableByRad.P α → solvableByRad.P β → solvableByRad.P γ
This theorem, called `solvableByRad.induction2`, states that for any field `F`, any algebra `E` over `F`, and any elements `α`, `β`, and `γ` from the intermediate field of solvable-by-radicals elements over `F` in `E`, if `γ` is in the field generated by `F`, `α`, and `β`, and if the minimal polynomial of `α` and `β` over `F` has a Galois group which is solvable (as captured by `solvableByRad.P α` and `solvableByRad.P β`), then the minimal polynomial of `γ` over `F` also has a Galois group that is solvable (as captured by `solvableByRad.P γ`). In simpler terms, this theorem is an induction step that helps us prove that an element is solvable by radicals if it lies in the field generated by two other elements that are solvable by radicals.
More concisely: If `F` is a field, `E` is an algebra over `F`, `α`, `β`, and `γ` are elements in the intermediate field of solvable-by-radicals elements over `F` in `E`, `γ` is in the field generated by `F`, `α`, and `β`, and the minimal polynomials of `α` and `β` have solvable Galois groups, then the minimal polynomial of `γ` also has a solvable Galois group.
|
solvableByRad.induction1
theorem solvableByRad.induction1 :
∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E]
{α β : ↥(solvableByRad F E)}, β ∈ F⟮α⟯ → solvableByRad.P α → solvableByRad.P β
This theorem, `solvableByRad.induction1`, states that for any fields `F` and `E` with `F` being a subfield of `E`, and for any two elements `α` and `β` in the intermediate field of solvable-by-radicals elements from `F` to `E`, if `β` is an element of the field generated by `F` and `α`, and the minimal polynomial of `α` over `F` has a solvable Galois group (i.e., `solvableByRad.P α` holds), then the minimal polynomial of `β` over `F` also has a solvable Galois group (i.e., `solvableByRad.P β` also holds). This theorem serves as an auxiliary induction lemma used in the proof of the statement that all elements in the intermediate field of solvable-by-radicals elements are solvable by radicals.
More concisely: If `F` is a subfield of `E`, `α` and `β` are elements in the intermediate field of solvable-by-radicals elements from `F` to `E`, `β` is in the field generated by `F` and `α`, and the minimal polynomial of `α` over `F` has a solvable Galois group, then the minimal polynomial of `β` over `F` also has a solvable Galois group.
|