Polynomial.Gal.galActionHom_bijective_of_prime_degree'
theorem Polynomial.Gal.galActionHom_bijective_of_prime_degree' :
∀ {p : Polynomial ℚ},
Irreducible p →
p.natDegree.Prime →
Fintype.card ↑(p.rootSet ℝ) + 1 ≤ Fintype.card ↑(p.rootSet ℂ) →
Fintype.card ↑(p.rootSet ℂ) ≤ Fintype.card ↑(p.rootSet ℝ) + 3 →
Function.Bijective ⇑(Polynomial.Gal.galActionHom p ℂ)
This theorem states that for any irreducible polynomial 'p' with coefficients in the set of rational numbers, if 'p' has a prime natural degree, and the number of its real roots plus one is less than or equal to the number of its complex roots, and also the number of its complex roots is less than or equal to the number of its real roots plus three, then the Galois action on the complex roots of 'p' is a bijective function. In simpler terms, if an irreducible polynomial of prime degree has between 1 and 3 non-real (complex) roots, the Galois group acting on the roots covers every permutation of the roots and each permutation exactly once, making it a "full" Galois group.
More concisely: If an irreducible polynomial of prime degree over the rational numbers has at most three non-real roots, then its Galois group acts transitively and bijectively on its complex roots.
|
Polynomial.Gal.card_complex_roots_eq_card_real_add_card_not_gal_inv
theorem Polynomial.Gal.card_complex_roots_eq_card_real_add_card_not_gal_inv :
∀ (p : Polynomial ℚ),
(p.rootSet ℂ).toFinset.card =
(p.rootSet ℝ).toFinset.card +
((Polynomial.Gal.galActionHom p ℂ)
((Polynomial.Gal.restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))).support.card
This theorem states that for any polynomial with rational coefficients, the number of its complex roots is equal to the sum of the number of its real roots and the number of roots not fixed by complex conjugation. In other words, it divides the complex roots of the polynomial into real roots and non-real roots (those that are affected by complex conjugation, thus having some imaginary component). This is expressed in Lean by counting the cardinality of the root sets of the polynomial in the complex and real numbers, and the number of roots that are not invariant under the action of the Galois group of the polynomial, when this action is induced by complex conjugation.
More concisely: The number of complex roots of a polynomial with rational coefficients equals the sum of its real roots and the number of non-conjugate complex roots.
|
Polynomial.Gal.galActionHom_bijective_of_prime_degree
theorem Polynomial.Gal.galActionHom_bijective_of_prime_degree :
∀ {p : Polynomial ℚ},
Irreducible p →
p.natDegree.Prime →
Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + 2 →
Function.Bijective ⇑(Polynomial.Gal.galActionHom p ℂ)
This theorem states that for any irreducible polynomial `p` with rational coefficients, if the degree of `p` is prime and there are two roots of `p` that are complex but not real (i.e., the number of complex roots is two more than the number of real roots), then the Galois group of `p` (considered as a permutation group acting on the roots of `p` in the complex numbers) is a full group. In other words, the map from the Galois group to the group of permutations of the complex roots, given by the action of the Galois group, is a bijection: each element of the Galois group corresponds to a unique permutation of the roots, and each permutation of the roots is achieved by some element of the Galois group.
More concisely: If `p` is an irreducible polynomial with rational coefficients of prime degree having exactly two more complex roots than real ones, then the Galois group of `p` acts faithfully on its complex roots.
|
Complex.exists_root
theorem Complex.exists_root : ∀ {f : Polynomial ℂ}, 0 < f.degree → ∃ z, f.IsRoot z
The theorem states the **Fundamental Theorem of Algebra**: every non-constant complex polynomial has at least one root. Here, `f` represents a complex polynomial and `f.degree` refers to the degree of the polynomial. The theorem asserts that if the degree of `f` is greater than 0 (meaning `f` is not a constant polynomial), then there exists a complex number `z` such that `z` is a root of the polynomial `f`. In other words, when the polynomial `f` is evaluated at `z`, the result is 0.
More concisely: Every non-constant complex polynomial has at least one complex root.
|