Polynomial.splits_map_iff
theorem Polynomial.splits_map_iff :
∀ {F : Type u} {K : Type v} {L : Type w} [inst : CommRing K] [inst_1 : Field L] [inst_2 : Field F] (i : K →+* L)
(j : L →+* F) {f : Polynomial K}, Polynomial.Splits j (Polynomial.map i f) ↔ Polynomial.Splits (j.comp i) f
This theorem states that for any given polynomial `f` over a commutative ring `K`, and ring homomorphisms `i` from `K` to a field `L` and `j` from `L` to a field `F`, the polynomial `f` splits over `F` via the map `j` composed with `i` if and only if the polynomial `f` mapped from `K` to `L` via `i`, splits over `F` via `j`. In other words, whether a polynomial splits does not depend on the order in which the ring homomorphisms are applied.
More concisely: For any polynomial `f` over a commutative ring `K` and ring homomorphisms `i : K -> L` to a field `L` and `j : L -> F` to a field `F`, if `f` splits over `F` via `j` composed with `i`, then `f` also splits over `F` via `i` composed with `j`. Conversely, if `f` splits over `F` via `i` composed with `j`, then it splits over `F` via `j` composed with `i`. Thus, the splitting of a polynomial over a field is independent of the order of the homomorphisms.
|
Polynomial.splits_X_sub_C
theorem Polynomial.splits_X_sub_C :
∀ {K : Type v} {L : Type w} [inst : CommRing K] [inst_1 : Field L] (i : K →+* L) {x : K},
Polynomial.Splits i (Polynomial.X - Polynomial.C x)
The theorem `Polynomial.splits_X_sub_C` states that for any commutative ring `K`, any field `L`, and any ring homomorphism `i` from `K` to `L`, the polynomial `X - C x` (where `X` represents the polynomial variable and `C x` is the constant polynomial `x`) splits over field `L`. In other words, the polynomial `X - C x` is either zero or all of its irreducible factors have degree 1 in the field `L`.
More concisely: For any commutative ring K, field L, and ring homomorphism i from K to L, the polynomial X - i(C) in L[X] splits completely into linear factors.
|
Polynomial.splits_of_splits_id
theorem Polynomial.splits_of_splits_id :
∀ {K : Type v} {L : Type w} [inst : Field K] [inst_1 : Field L] (i : K →+* L) {f : Polynomial K},
Polynomial.Splits (RingHom.id K) f → Polynomial.Splits i f
The theorem `Polynomial.splits_of_splits_id` states that for any two fields `K` and `L`, and a ring homomorphism `i` from `K` to `L`, if a polynomial `f` over the field `K` splits over `K` itself (meaning that it is either the zero polynomial or all of its irreducible factors have a degree of 1), then `f` also splits over `L` under the ring homomorphism `i`. This implies that the property of being a split polynomial is preserved under ring homomorphisms.
More concisely: If a polynomial over a field splits in the field, then it splits in any larger field under a ring homomorphism.
|
Polynomial.prod_roots_eq_coeff_zero_of_monic_of_split
theorem Polynomial.prod_roots_eq_coeff_zero_of_monic_of_split :
∀ {K : Type v} [inst : Field K] {P : Polynomial K},
P.Monic → Polynomial.Splits (RingHom.id K) P → P.coeff 0 = (-1) ^ P.natDegree * P.roots.prod
The theorem `Polynomial.prod_roots_eq_coeff_zero_of_monic_of_split` states that for any field `K` and any monic polynomial `P` over `K`, if `P` splits (which means it is either zero or all of its irreducible factors have a degree of 1), then the coefficient of the zeroth-degree term of `P` equals the product of the roots of `P` times `(-1)` raised to the power of the natural degree of `P`.
More concisely: If `K` is a field and monic polynomial `P` over `K` splits, then the constant term of `P` equals the product of its zeroth-degree roots and (-1)^n, where n is the degree of `P`.
|
Polynomial.natDegree_eq_card_roots'
theorem Polynomial.natDegree_eq_card_roots' :
∀ {K : Type v} {L : Type w} [inst : CommRing K] [inst_1 : Field L] {p : Polynomial K} {i : K →+* L},
Polynomial.Splits i p → (Polynomial.map i p).natDegree = Multiset.card (Polynomial.map i p).roots
This theorem states that for any commutative ring `K`, any field `L`, any polynomial `p` over `K`, and any ring homomorphism `i` from `K` to `L`, if the polynomial `p` splits via `i`, then the natural degree of the polynomial obtained by mapping `p` across `i` is equal to the cardinality of the multiset of roots of the mapped polynomial. In other words, if a polynomial can be factored such that all its irreducible factors have degree 1, then the natural degree of the polynomial in the field `L` is equal to the number of its roots in `L` including their multiplicities.
More concisely: For any commutative ring `K`, field `L`, ring homomorphism `i` from `K` to `L`, and polynomial `p` over `K`, if `p` splits in `L` via `i` with all irreducible factors having degree 1, then the degree of the mapped polynomial equals the number of roots of `p` in `L` including multiplicities.
|
Polynomial.exists_root_of_splits
theorem Polynomial.exists_root_of_splits :
∀ {K : Type v} {L : Type w} [inst : Field K] [inst_1 : Field L] (i : K →+* L) {f : Polynomial K},
Polynomial.Splits i f → f.degree ≠ 0 → ∃ x, Polynomial.eval₂ i x f = 0
This theorem states that for any fields `K` and `L` and a ring homomorphism `i` from `K` to `L`, if a polynomial `f` with coefficients in `K` splits according to `i` and the degree of `f` is not zero, then there exists a root `x` in `L` where `x` is such that when we evaluate the polynomial `f` at `x` using the ring homomorphism `i`, we get zero.
In other words, if a non-zero degree polynomial over one field splits when mapped to another field using a ring homomorphism, then there exist roots in the target field. Here, a polynomial is said to "split" if it is zero or all its irreducible factors have a degree of 1.
More concisely: Given fields `K` and `L` and a ring homomorphism `i` from `K` to `L`, if a non-zero polynomial `f` in `K[x]` splits over `L` via `i`, then there exists a root of `f` in `L` when evaluated through `i`.
|
Polynomial.adjoin_rootSet_eq_range
theorem Polynomial.adjoin_rootSet_eq_range :
∀ {R : Type u_1} {K : Type v} {L : Type w} [inst : CommRing R] [inst_1 : Field K] [inst_2 : Field L]
[inst_3 : Algebra R K] [inst_4 : Algebra R L] {p : Polynomial R},
Polynomial.Splits (algebraMap R K) p →
∀ (f : K →ₐ[R] L), Algebra.adjoin R (p.rootSet L) = f.range ↔ Algebra.adjoin R (p.rootSet K) = ⊤
The theorem `Polynomial.adjoin_rootSet_eq_range` states that for any commutative rings `R`, `K`, and `L` with `K` and `L` being fields and `R` being an algebra over both `K` and `L`, and for any polynomial `p` over `R` that splits over `K`, for any algebra homomorphism `f` from `K` to `L`, the subalgebra of `L` generated by the set of roots of `p` in `L` is the range of `f` if and only if the subalgebra of `K` generated by the set of roots of `p` in `K` is the entire space `K`. In other words, the roots of a polynomial in a field generate the whole field if and only if they generate the entire range of any algebra homomorphism from that field to another.
More concisely: For a polynomial `p` over a commutative ring `R` that splits over fields `K` and `L`, the subalgebras of `L` generated by the roots of `p` in `L` and of `K` generated by the roots of `p` in `K` are equal if and only if the latter is the entire field `K`.
|
Polynomial.splits_iff_card_roots
theorem Polynomial.splits_iff_card_roots :
∀ {K : Type v} [inst : Field K] {p : Polynomial K},
Polynomial.Splits (RingHom.id K) p ↔ Multiset.card p.roots = p.natDegree
This theorem states that a polynomial over a field splits if and only if the number of its roots, including their multiplicities, is equal to its degree. Here, a polynomial is said to split if it is either zero or all of its irreducible factors have degree 1. The roots of the polynomial are computed non-computationally, giving a multiset that includes all the roots along with their multiplicities. The degree of the polynomial is forced to a natural number, with the degree of the zero polynomial defined as 0. The identity mapping of the field is used in the definition of a splitting polynomial.
More concisely: A polynomial over a field is splitting if and only if it has exactly degree-many roots, counted with multiplicity.
|
Polynomial.splits_C
theorem Polynomial.splits_C :
∀ {K : Type v} {L : Type w} [inst : CommRing K] [inst_1 : Field L] (i : K →+* L) (a : K),
Polynomial.Splits i (Polynomial.C a)
The theorem `Polynomial.splits_C` states that for any commutative ring `K` and any field `L`, given any ring homomorphism `i` from `K` to `L` and any element `a` in `K`, the constant polynomial `a` splits with respect to `i`. That is, the polynomial obtained from mapping all coefficients of the constant polynomial `a` via `i` is either zero, or all of its irreducible factors (if any) have degree 1.
More concisely: For any commutative ring homomorphism from a ring K to a field L and any element a in K, the constant polynomial a over K splits in L with irreducible factors of degree at most 1.
|
Polynomial.splits_of_degree_le_one
theorem Polynomial.splits_of_degree_le_one :
∀ {K : Type v} {L : Type w} [inst : CommRing K] [inst_1 : Field L] (i : K →+* L) {f : Polynomial K},
f.degree ≤ 1 → Polynomial.Splits i f
The theorem `Polynomial.splits_of_degree_le_one` states that for all commutative rings `K` and fields `L`, and a given homomorphism `i` from `K` to `L`, if the degree of a polynomial `f` from `K` is less than or equal to 1, then the polynomial `f` splits over `L`. In other words, if a polynomial has a degree of 1 or less, then it can be factored into linear polynomials in the field `L`.
More concisely: For any commutative rings K and fields L, and homomorphism i from K to L, polynomials of degree less than or equal to 1 in K split into linear factors in L.
|
Polynomial.splits_of_splits_of_dvd
theorem Polynomial.splits_of_splits_of_dvd :
∀ {K : Type v} {L : Type w} [inst : Field K] [inst_1 : Field L] (i : K →+* L) {f g : Polynomial K},
f ≠ 0 → Polynomial.Splits i f → g ∣ f → Polynomial.Splits i g
This theorem states that for any two polynomials `f` and `g` over a field `K`, with `K` being mapped to a field `L` through a ring homomorphism `i`, if `f` is not the zero polynomial and `f` splits over `L` (meaning `f` is a zero polynomial or all of its irreducible factors have degree 1 when mapped to `L`), and if `g` divides `f`, then `g` also splits over `L`. Simply, if a polynomial is divisible by another polynomial and the original one splits into linear factors, then the dividing polynomial also splits into linear factors.
More concisely: If a polynomial `f` over a field `K` splits into linear factors over an extension field `L` via a ring homomorphism `i`, and `g` is a divisor of `f` over `K`, then `g` also splits into linear factors over `L`.
|
Polynomial.splits_one
theorem Polynomial.splits_one :
∀ {K : Type v} {L : Type w} [inst : CommRing K] [inst_1 : Field L] (i : K →+* L), Polynomial.Splits i 1
The theorem `Polynomial.splits_one` states that for any commutative ring `K` and any field `L`, and any ring homomorphism `i` from `K` to `L`, the number `1` is a "split" polynomial. This means that when you map `1` from `K` to `L`, you either get zero or all of its irreducible factors in `L` have a polynomial degree of `1`.
More concisely: For any commutative ring K and field L, and any ring homomorphism i from K to L, the element 1 in K maps to a polynomial with degree 1 or a root in L.
|
Polynomial.sum_roots_eq_nextCoeff_of_monic_of_split
theorem Polynomial.sum_roots_eq_nextCoeff_of_monic_of_split :
∀ {K : Type v} [inst : Field K] {P : Polynomial K},
P.Monic → Polynomial.Splits (RingHom.id K) P → P.nextCoeff = -P.roots.sum
This theorem states that if `P` is a monic polynomial which splits (meaning it is either a zero polynomial or all of its irreducible factors have a degree of 1), then the next coefficient of `P` is equal to the negative sum of the roots of `P`. The splitting of the polynomial is in the field `K` with respect to the identity ring homomorphism.
In mathematical terms, for any field `K` and a monic polynomial `P` in that field, if `P` splits then the coefficient of the second to highest degree term in `P` is equal to the negative sum of the roots of `P`.
More concisely: If `P` is a monic polynomial over a field `K` that splits, then the coefficient of the second highest degree term in `P` equals the negative sum of its roots.
|
Polynomial.map_rootOfSplits
theorem Polynomial.map_rootOfSplits :
∀ {K : Type v} {L : Type w} [inst : Field K] [inst_1 : Field L] (i : K →+* L) {f : Polynomial K}
(hf : Polynomial.Splits i f) (hfd : f.degree ≠ 0), Polynomial.eval₂ i (Polynomial.rootOfSplits i hf hfd) f = 0
The theorem `Polynomial.map_rootOfSplits` states that for any field `K`, another field `L`, and a ring homomorphism `i` from `K` to `L`, given a polynomial `f` over `K` that splits under `i`, and assuming that the degree of `f` is not zero, if you evaluate `f` at the root produced by `Polynomial.rootOfSplits` using the ring homomorphism `i`, the result is zero. In other words, `Polynomial.rootOfSplits` indeed produces a root of `f` when `f` is mapped into `L` using `i`.
More concisely: Given a field homomorphism `i` from `K` to `L`, a polynomial `f` of non-zero degree over `K` that splits at some `α` in `K`, the image `i(α)` is a root of the polynomial `i(f)` in `L`.
|
Polynomial.eq_prod_roots_of_monic_of_splits_id
theorem Polynomial.eq_prod_roots_of_monic_of_splits_id :
∀ {K : Type v} [inst : Field K] {p : Polynomial K},
p.Monic →
Polynomial.Splits (RingHom.id K) p → p = (Multiset.map (fun a => Polynomial.X - Polynomial.C a) p.roots).prod
The theorem states that for any field `K` and any monic polynomial `p` over `K`, if `p` splits over `K` (meaning it is either the zero polynomial or all of its irreducible factors have degree 1), then `p` can be expressed as the product of linear factors `(Polynomial.X - Polynomial.C a)`, where `a` is a root of `p`. Each root `a` is included in the product with multiplicity equal to its multiplicity as a root of `p`. In mathematical terms, this corresponds to the statement that a monic polynomial is equal to the product of `(X - a_i)` over all its roots `a_i`.
More concisely: A monic polynomial over a field that splits into linear factors is equal to the product of these factors, where each factor corresponds to a root with the root's multiplicity.
|
Polynomial.splits_mul
theorem Polynomial.splits_mul :
∀ {K : Type v} {L : Type w} [inst : CommRing K] [inst_1 : Field L] (i : K →+* L) {f g : Polynomial K},
Polynomial.Splits i f → Polynomial.Splits i g → Polynomial.Splits i (f * g)
The theorem `Polynomial.splits_mul` states that for every commutative ring `K` and field `L`, and for every ring homomorphism `i` from `K` to `L`, if a polynomial `f` and a polynomial `g` (both from `K`) each split over `L` under the homomorphism `i`, then their product `f * g` also splits over `L` under the same homomorphism. Here, a polynomial is said to "split" if it is zero or all of its irreducible factors have degree 1.
More concisely: For every commutative ring K and field L, if polynomials f and g from K each split over L under a ring homomorphism i, then their product f * g splits over L under i as well.
|
Polynomial.natDegree_eq_card_roots
theorem Polynomial.natDegree_eq_card_roots :
∀ {K : Type v} {L : Type w} [inst : Field K] [inst_1 : Field L] {p : Polynomial K} {i : K →+* L},
Polynomial.Splits i p → p.natDegree = Multiset.card (Polynomial.map i p).roots
This theorem states that for any given polynomial `p` over a field `K` and a ring homomorphism `i` from `K` to another field `L`, if the polynomial `p` splits under the ring homomorphism `i` (meaning that it is either zero or all of its irreducible factors have degree one), then the natural degree of the polynomial `p` is equal to the cardinality of the multiset of roots of the polynomial `p` when mapped via `i`. The natural degree of a polynomial is the degree forced to natural numbers, where the degree of the zero polynomial is defined as zero. The cardinality of a multiset is the sum of the multiplicities of all its elements, and the roots of a polynomial are all the solutions of the polynomial equation, including their multiplicities.
More concisely: If polynomial `p` over field `K` splits under ring homomorphism `i` from `K` to field `L`, then the natural degree of `p` equals the cardinality of the multiset of roots of `p` when mapped via `i`.
|
Polynomial.eq_prod_roots_of_splits
theorem Polynomial.eq_prod_roots_of_splits :
∀ {K : Type v} {L : Type w} [inst : Field K] [inst_1 : Field L] {p : Polynomial K} {i : K →+* L},
Polynomial.Splits i p →
Polynomial.map i p =
Polynomial.C (i p.leadingCoeff) *
(Multiset.map (fun a => Polynomial.X - Polynomial.C a) (Polynomial.map i p).roots).prod
The theorem `Polynomial.eq_prod_roots_of_splits` states that for any field `K` and `L`, along with a polynomial `p` from `K` and a ring homomorphism `i` from `K` to `L`, if the polynomial `p` splits via the ring homomorphism `i`, then the polynomial `p`, when mapped using `i`, can be expressed as the product of the constant polynomial of the leading coefficient of `p` (mapped via `i`) and the product of polynomials each of which is the difference between the polynomial variable `X` and the constant polynomial of a root of the mapped polynomial `p`. The roots are taken from the multiset of roots of the mapped polynomial `p`.
More concisely: If a polynomial `p` from field `K` splits via a ring homomorphism `i` from `K` to `L`, then `p` maps to the product of the leading coefficient of `p` (mapped via `i`) and the product of the differences between `X` and the images under `i` of the roots of `p`.
|
Polynomial.rootOfSplits'_eq_rootOfSplits
theorem Polynomial.rootOfSplits'_eq_rootOfSplits :
∀ {K : Type v} {L : Type w} [inst : Field K] [inst_1 : Field L] (i : K →+* L) {f : Polynomial K}
(hf : Polynomial.Splits i f) (hfd : (Polynomial.map i f).degree ≠ 0),
Polynomial.rootOfSplits' i hf hfd = Polynomial.rootOfSplits i hf ⋯
The theorem `Polynomial.rootOfSplits'_eq_rootOfSplits` states that for any field mapping `i` from `K` to `L`, and any polynomial `f` from `K` such that `f` splits via `i` and the degree of the mapped polynomial `i(f)` is non-zero, the function `Polynomial.rootOfSplits'` produces the same result as `Polynomial.rootOfSplits`. In other words, both methods identify the same root in `L` for the polynomial `f` that splits.
More concisely: For any field extension `i : K → L` and polynomial `f : K` with non-zero degree and roots `r₁, r₂` in `K` such that `i(r₁)` and `i(r₂)` are the roots of `i(f)` in `L`, `Polynomial.rootOfSplits' i f` equals `{ x : L | ∃ r in K, i(x) = r and x = rootOfSplits i f}` (the set of roots of `i(f)` in `L`).
|
Polynomial.Splits.def
theorem Polynomial.Splits.def :
∀ {K : Type v} {L : Type w} [inst : Field K] [inst_1 : Field L] {i : K →+* L} {f : Polynomial K},
Polynomial.Splits i f → f = 0 ∨ ∀ {g : Polynomial L}, Irreducible g → g ∣ Polynomial.map i f → g.degree = 1
This theorem is about polynomials over a field. It states that for any field K and L, and any ring homomorphism from K to L, if a polynomial `f` from field K "splits", then either the polynomial `f` is zero or for every irreducible polynomial `g` from field L, if `g` divides the polynomial obtained by mapping `f` through the ring homomorphism, then the degree of `g` is 1. In this context, a polynomial "splits" if it is either zero or all of its irreducible factors have a degree of 1.
More concisely: Given any field homomorphism between fields K and L, if a polynomial f from K splits over L, then for every irreducible factor g of the image of f under the homomorphism, the degree of g is equal to 1.
|
Polynomial.splits_id_iff_splits
theorem Polynomial.splits_id_iff_splits :
∀ {K : Type v} {L : Type w} [inst : CommRing K] [inst_1 : Field L] (i : K →+* L) {f : Polynomial K},
Polynomial.Splits (RingHom.id L) (Polynomial.map i f) ↔ Polynomial.Splits i f
This theorem states that for all types `K` and `L`, where `K` is a commutative ring and `L` is a field, and for every ring homomorphism `i` from `K` to `L`, and for any polynomial `f` in `K`, the polynomial `f` splits over `L` when mapped by `i` and then considered under the identity ring homomorphism on `L` if and only if the polynomial `f` splits over `L` under the ring homomorphism `i`. In other words, the splitting of the polynomial as it is mapped to `L` is independent of whether we then consider it under the identity map on `L`.
In mathematical terms, a polynomial `f` "splits" if it is either the zero polynomial, or all of its irreducible factors have degree 1. This theorem is about the equivalence of split conditions between the original polynomial and its version after ring homomorphism.
More concisely: For any commutative ring `K`, field `L`, ring homomorphism `i` from `K` to `L`, and polynomial `f` in `K`, the polynomial `f` splits over `L` under `i` if and only if it splits over `L` after applying `i` and the identity homomorphism on `L`.
|
Polynomial.splits_prod
theorem Polynomial.splits_prod :
∀ {K : Type v} {L : Type w} [inst : CommRing K] [inst_1 : Field L] (i : K →+* L) {ι : Type u} {s : ι → Polynomial K}
{t : Finset ι}, (∀ j ∈ t, Polynomial.Splits i (s j)) → Polynomial.Splits i (t.prod fun x => s x)
The theorem `Polynomial.splits_prod` states that for any commutative ring `K`, any field `L`, and any ring homomorphism from `K` to `L`, given a function `s` that maps any type `ι` to a polynomial in `K`, and a finite set `t` of elements of type `ι`, if every polynomial `s j`, for `j` in `t`, splits according to the ring homomorphism `i`, then the product of the polynomials `s x` for `x` in `t` also splits according to the ring homomorphism `i`. In other words, if all polynomials in a finite set split under a certain ring homomorphism, then their product also splits under the same ring homomorphism.
More concisely: Given a commutative ring K, a field L, a ring homomorphism i from K to L, a function s mapping type ι to polynomials in K, and a finite set t of elements from ι such that every polynomial s j splits under i for j in t, then the product of the polynomials s x for x in t also splits under i.
|
Polynomial.splits_iff
theorem Polynomial.splits_iff :
∀ {K : Type v} {L : Type w} [inst : Field K] [inst_1 : Field L] (i : K →+* L) (f : Polynomial K),
Polynomial.Splits i f ↔ f = 0 ∨ ∀ {g : Polynomial L}, Irreducible g → g ∣ Polynomial.map i f → g.degree = 1
This theorem is about polynomials over a field. It states that for any field mapping `i` from `K` to `L` and any polynomial `f` in `K`, `f` splits with respect to `i` if and only if `f` equals zero or for every irreducible polynomial `g` in `L`, if `g` divides the result of mapping `f` through `i`, then `g` has degree 1. In other words, a polynomial is said to split if it is either zero or all of its irreducible factors that divide the mapped polynomial have a degree of one.
More concisely: A polynomial over a field `f` splits with respect to a field mapping `i` from `K` to `L` if and only if `f` is the zero polynomial or all irreducible factors of `i(f)` in `L` have degree 1.
|
Polynomial.exists_root_of_splits'
theorem Polynomial.exists_root_of_splits' :
∀ {K : Type v} {L : Type w} [inst : CommRing K] [inst_1 : Field L] (i : K →+* L) {f : Polynomial K},
Polynomial.Splits i f → (Polynomial.map i f).degree ≠ 0 → ∃ x, Polynomial.eval₂ i x f = 0
This theorem states that if a polynomial `f` of type `K` splits over a field `L`, denoted as `Polynomial.Splits i f`, where `i` is a ring homomorphism from `K` to `L`, and if the degree of the polynomial `f` mapped into `L` is non-zero, then there exists a root `x` in the field `L` such that the polynomial `f` evaluates to zero at `x`, i.e., `Polynomial.eval₂ i x f = 0`. In other words, a non-zero degree polynomial that splits over a field will always have at least one root in that field.
More concisely: If a polynomial of non-zero degree `f` splits over a field `L` via homomorphism `i`, then there exists a root `x` in `L` such that `f(x) = 0`.
|
Polynomial.splits_comp_of_splits
theorem Polynomial.splits_comp_of_splits :
∀ {R : Type u_1} {K : Type v} {L : Type w} [inst : CommRing R] [inst_1 : Field K] [inst_2 : Field L] (i : R →+* K)
(j : K →+* L) {f : Polynomial R}, Polynomial.Splits i f → Polynomial.Splits (j.comp i) f
The theorem `Polynomial.splits_comp_of_splits` states that for any given types `R`, `K`, and `L`, with `R` being a commutative ring and `K` and `L` being fields, if a polynomial `f` from the ring `R` splits over the field `K` under a ring homomorphism `i`, then it also splits over the field `L` under the composition of ring homomorphisms `j` and `i`. In simpler terms, if a polynomial splits over one field, it will also split over another when we apply a composition of functions that map elements between the fields and the original ring.
More concisely: If a polynomial over a commutative ring splits over a field under a ring homomorphism, then it splits over another field under the composition of ring homomorphisms.
|