Polynomial.aeval_algHom
theorem Polynomial.aeval_algHom :
∀ {R : Type u} {A : Type z} {B : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
[inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →ₐ[R] B) (x : A),
Polynomial.aeval (f x) = f.comp (Polynomial.aeval x)
The theorem `Polynomial.aeval_algHom` states that for any commutative semiring `R`, semirings `A` and `B`, and any algebra structure over `R` on `A` and `B`, given an algebra homomorphism `f` from `A` to `B` and an element `x` of `A`, the algebra evaluation of `f(x)` is equal to the composition of `f` and the algebra evaluation at `x`. In other words, applying the algebra homomorphism first and then performing the algebra evaluation is the same as performing the algebra evaluation first and then applying the algebra homomorphism.
More concisely: For any commutative semirings R, semirings A and B, algebra structures on A and B over R, algebra homomorphism f from A to B, and element x in A, we have f(α(x)) = α(f(x)), where α denotes algebra evaluation.
|
Polynomial.aeval_X_pow
theorem Polynomial.aeval_X_pow :
∀ {R : Type u} {A : Type z} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (x : A) {n : ℕ},
(Polynomial.aeval x) (Polynomial.X ^ n) = x ^ n
The theorem `Polynomial.aeval_X_pow` states that for any commutative semiring `R`, any semiring `A`, and any algebra `A` over `R`, giving any element `x` from `A` and any natural number `n`, the application of the unique `R`-algebra homomorphism (denoted as `Polynomial.aeval x`) to the `n`-th power of the polynomial variable `Polynomial.X` is equal to the `n`-th power of `x`. In other words, when we evaluate the `n`-th power of the polynomial variable at `x`, we get the `n`-th power of `x`. This is a property of algebra homomorphisms that map polynomial expressions in `R[X]` to members of an `R`-algebra `A` by replacing the polynomial variable `X` with a specific value `x` from `A`.
More concisely: For any commutative semiring `R`, semiring `A` with an `R`-algebra structure, and `x` in `A`, the `R`-algebra homomorphism `Polynomial.aeval` satisfies `Polynomial.aeval (X ^ n) x = x ^ n` for all natural numbers `n`.
|
Polynomial.aeval_def
theorem Polynomial.aeval_def :
∀ {R : Type u} {A : Type z} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (x : A)
(p : Polynomial R), (Polynomial.aeval x) p = Polynomial.eval₂ (algebraMap R A) x p
This theorem states that for any commutative semiring `R`, semiring `A`, algebra structure between `R` and `A`, element `x` from `A`, and a polynomial `p` with coefficients in `R`, the application of the algebra homomorphism (`Polynomial.aeval x`) to the polynomial `p` is equal to the evaluation of the polynomial `p` at `x` via the ring homomorphism (`algebraMap R A`). In other words, it ensures that evaluating the polynomial through the algebra homomorphism is the same as evaluating it at a specific point using the ring homomorphism provided by the algebra structure.
More concisely: For any commutative semiring `R`, semiring `A` with an algebra structure over `R`, element `x` from `A`, and polynomial `p` with coefficients in `R`, the application of the algebra homomorphism `Polynomial.aeval x` to `p` equals the evaluation of `p` at `x` via the ring homomorphism `algebraMap R A`.
|
Polynomial.algHom_ext
theorem Polynomial.algHom_ext :
∀ {R : Type u} {B : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring B] [inst_2 : Algebra R B]
{f g : Polynomial R →ₐ[R] B}, f Polynomial.X = g Polynomial.X → f = g
The theorem `Polynomial.algHom_ext` states that for any two algebra homomorphisms `f` and `g` from the set of polynomials over a commutative semiring `R` to a semiring `B`, under the condition that `R` is an algebra over `B`, if `f` and `g` map the polynomial indeterminate `X` to the same element, then `f` and `g` are equal. In other words, the behavior of an algebra homomorphism on the polynomial indeterminate completely determines the homomorphism.
More concisely: If `R` is a commutative semiring where `R` is an algebra over a semiring `B`, and `f` and `g` are algebra homomorphisms from `R[X]` to `B` with `f X = g X`, then `f = g`.
|
Polynomial.aevalTower_X
theorem Polynomial.aevalTower_X :
∀ {R : Type u} {S : Type v} {A' : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring A']
[inst_2 : CommSemiring S] [inst_3 : Algebra S R] [inst_4 : Algebra S A'] (g : R →ₐ[S] A') (y : A'),
(Polynomial.aevalTower g y) Polynomial.X = y
The theorem `Polynomial.aevalTower_X` states that for any commutative semirings `R`, `S`, `A'` and any algebra structure on `R` and `A'` over `S`, and for any algebra homomorphism `g : R →ₐ[S] A'` and any element `y : A'`, the evaluation of the polynomial variable, or indeterminate (which is denoted by `Polynomial.X`), under the `Polynomial.aevalTower` function with parameters `g` and `y`, is equal to `y`. In other words, substituting `y` for `Polynomial.X` in a polynomial over `R` using the algebra homomorphism `g` results in `y`.
More concisely: For any commutative semirings R, S, and algebra structures on R and A' over S, and for any algebra homomorphism g : R -> A' and any element y : A', the evaluation of the indeterminate X in a polynomial over R using g and y is equivalent to y.
|
Polynomial.coe_aeval_eq_eval
theorem Polynomial.coe_aeval_eq_eval :
∀ {R : Type u} [inst : CommSemiring R] (r : R), ⇑(Polynomial.aeval r) = Polynomial.eval r
This theorem states that for any given commutative semiring R and an element r of the semiring, the algebra homomorphism created by applying the polynomial `aeval` function to r is equivalent to simply evaluating the polynomial at r using the `eval` function. In more technical terms, it asserts that in the context of a commutative semiring, the map induced by the `aeval` function and the result of the `eval` function are the same.
More concisely: For any commutative semiring R and element r, the homomorphism induced by the `aeval` function of polynomial evaluation equals the result of directly evaluating the polynomial at r.
|
Polynomial.aeval_C
theorem Polynomial.aeval_C :
∀ {R : Type u} {A : Type z} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (x : A) (r : R),
(Polynomial.aeval x) (Polynomial.C r) = (algebraMap R A) r
The `Polynomial.aeval_C` theorem states that for all types `R` and `A`, where `R` is a commutative semiring, `A` is a semiring, and `A` is an `R`-algebra, for any `x` in `A` and `r` in `R`, applying the `aeval` function (which is an `R`-algebra homomorphism) to `x` on the constant polynomial `C` of `r` equals the result of applying the algebra map from `R` to `A` on `r`. In other words, if you evaluate the constant polynomial `C` at `x` using `aeval`, you get the same result as if you simply mapped `r` from `R` to `A` using the algebra structure of `A`. This is equivalent to the mathematical statement that for any algebra $A$ over a commutative ring $R$, the evaluation homomorphism at any element $x \in A$ applied to a constant polynomial $C(r)$ is equal to the image of $r$ under the given ring homomorphism from $R$ to $A$.
More concisely: For any commutative semiring R, semiring A as an R-algebra, and x in A, the evaluation of the constant polynomial C(r) at x using aeval is equal to the application of the algebra map from R to A on r.
|
Algebra.adjoin_singleton_eq_range_aeval
theorem Algebra.adjoin_singleton_eq_range_aeval :
∀ (R : Type u) {A : Type z} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (x : A),
Algebra.adjoin R {x} = (Polynomial.aeval x).range
This theorem states that for any commutative semiring `R` and any semiring `A`, given an algebra structure on `A` over `R` and an element `x` from `A`, the subalgebra of `A` generated by `R` and the singleton set `{x}` is equal to the range of the algebra homomorphism defined by evaluating polynomials at `x`. In other words, every element in the minimal subalgebra that includes `{x}` can be obtained by taking a polynomial with coefficients in `R`, replacing the variable by `x`, and performing the resulting operations in `A`.
More concisely: For any commutative semiring `R`, semiring `A`, algebra structure on `A` over `R`, and element `x` in `A`, the subalgebra of `A` generated by `R` and `{x}` equals the image of the algebra homomorphism sending polynomials over `R` to their evaluations at `x` in `A`.
|
Polynomial.algHom_ext'
theorem Polynomial.algHom_ext' :
∀ {R : Type u} {A : Type z} {B : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
[inst_3 : Algebra R A] [inst_4 : Algebra R B] {f g : Polynomial A →ₐ[R] B},
f.comp Polynomial.CAlgHom = g.comp Polynomial.CAlgHom → f Polynomial.X = g Polynomial.X → f = g
This theorem, `Polynomial.algHom_ext'`, is an extensionality lemma for algebra maps out of `A'[X]` over a smaller base ring than `A'`. In more detail, it states that for any types `R`, `A`, and `B` with `R` a commutative semiring, `A` a semiring, and `B` a semiring, and `A` and `B` being algebras over `R`, if we have two algebra homomorphisms `f` and `g` from the polynomial ring in `A` to `B`, then if the composition of `f` and `Polynomial.CAlgHom` (which maps a scalar to a constant polynomial) equals the composition of `g` and `Polynomial.CAlgHom`, and `f` applied to the polynomial variable `X` equals `g` applied to `X`, then `f` and `g` are equal.
More concisely: If `R` is a commutative semiring, `A` and `B` are semirings and algebras over `R`, and `f` and `g` are algebra homomorphisms from the polynomial ring in `A` to `B` such that `Polynomial.CAlgHom ∘ f = Polynomial.CAlgHom ∘ g` and `f X = g X`, then `f = g`.
|
Polynomial.aeval_X
theorem Polynomial.aeval_X :
∀ {R : Type u} {A : Type z} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (x : A),
(Polynomial.aeval x) Polynomial.X = x
This theorem states that for any commutative semiring `R` and semiring `A`, given an `R`-algebra structure on `A` and any element `x` of `A`, the algebra homomorphism from the polynomial ring `R[X]` to `A` generated by evaluating `X` at `x` (as defined by `Polynomial.aeval`) sends the polynomial `X` (the polynomial indeterminate or variable) to `x`. In other words, applying this homomorphism to the polynomial `X` gives back the original `x` in `A` that was used to create the homomorphism. This theorem captures the intuition that a polynomial evaluation at a certain point replaces the variable of the polynomial with the point of evaluation.
More concisely: For any commutative semiring `R`, semiring `A`, `R`-algebra structure on `A`, and element `x` in `A`, the algebra homomorphism from `R[X]` to `A` generated by evaluating `X` at `x` maps the polynomial indeterminate `X` to `x`.
|
Polynomial.not_isUnit_X_sub_C
theorem Polynomial.not_isUnit_X_sub_C :
∀ {R : Type u} [inst : Ring R] [inst_1 : Nontrivial R] (r : R), ¬IsUnit (Polynomial.X - Polynomial.C r)
The theorem `Polynomial.not_isUnit_X_sub_C` states that for any type `R` that is a `Ring` and is `Nontrivial`, and for any real number `r`, the polynomial `X - C r`, where `X` is the polynomial variable and `C r` is the constant polynomial `r`, is not a unit. In other words, the polynomial `X - C r` does not have a two-sided inverse in the ring of polynomials over `R`.
More concisely: For any nontrivial ring R and real number r, the polynomial X - Cr is not a unit in the ring of polynomials over R.
|
Polynomial.aeval_one
theorem Polynomial.aeval_one :
∀ {R : Type u} {A : Type z} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (x : A),
(Polynomial.aeval x) 1 = 1
The theorem `Polynomial.aeval_one` states that for any given evaluation `x` of the variable in an `R`-algebra `A`, where `R` is a commutative semiring and `A` is a semiring, the unique `R`-algebra homomorphism from `R[X]` to `A` that sends `X` to `x`, when applied to the polynomial 1, produces 1. In other words, evaluating the polynomial 1 under any valuation in any `R`-algebra always gives back 1.
More concisely: For any commutative semiring `R`, `R`-algebra `A`, and evaluation `x` in `A`, the unique `R`-algebra homomorphism from `R[X]` to `A` maps the polynomial 1 to 1, i.e., `(�� heal x : R[X] →* A) 1 = 1`.
|
Polynomial.eval_mul_X_sub_C
theorem Polynomial.eval_mul_X_sub_C :
∀ {R : Type u} [inst : Ring R] {p : Polynomial R} (r : R),
Polynomial.eval r (p * (Polynomial.X - Polynomial.C r)) = 0
The theorem `Polynomial.eval_mul_X_sub_C` states that for any ring `R`, any polynomial `p` in `R`, and any `r` in `R`, if we evaluate the polynomial `p` multiplied by the difference of the polynomial variable `X` and the constant polynomial `r` at `r`, the result is always zero. This means that for any polynomial whose form is `p * (X - r)`, where `p` is a polynomial and `r` is a real number, evaluating it at `r` will result in zero. This is a critical step in the proof of the Cayley-Hamilton theorem, which states that every square matrix over a commutative ring is a root of its characteristic polynomial.
More concisely: For any polynomial `p` and constant `r` in a ring `R`, `p * (X - r)` evaluates to the zero polynomial at `r`.
|
Polynomial.C_eq_algebraMap
theorem Polynomial.C_eq_algebraMap :
∀ {R : Type u} [inst : CommSemiring R] (r : R), Polynomial.C r = (algebraMap R (Polynomial R)) r
The theorem `Polynomial.C_eq_algebraMap` asserts that for any commutative semiring `R` and any element `r` in `R`, the constant polynomial `r` in `R` is equivalent to the result of applying the algebra map to `r`, where the algebra map is considered from the ring `R` to the ring of polynomials over `R`. It's important to note that while the function `C` that gives the constant polynomial is defined even when `R` is not commutative, the `algebraMap` function is only available when `R` is a commutative semiring.
More concisely: For any commutative semiring `R` and element `r` in `R`, the constant polynomial `r` is equal to the image of `r` under the algebra map from `R` to the polynomial algebra over `R`.
|
Polynomial.aeval_algHom_apply
theorem Polynomial.aeval_algHom_apply :
∀ {R : Type u} {A : Type z} {B : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
[inst_3 : Algebra R A] [inst_4 : Algebra R B] {F : Type u_3} [inst_5 : FunLike F A B]
[inst_6 : AlgHomClass F R A B] (f : F) (x : A) (p : Polynomial R),
(Polynomial.aeval (f x)) p = f ((Polynomial.aeval x) p)
This theorem states that for any commutative semiring `R`, semirings `A` and `B`, algebra structures over `R` on `A` and `B`, a function-like object `F` from `A` to `B`, and an algebra homomorphism class for `F` from `R` to `A` to `B`, if you take any algebra homomorphism `f` from `F`, any element `x` from `A`, and any polynomial `p` with coefficients in `R`, then applying the polynomial `p` to the algebra homomorphism of `x` under `f` (i.e., `(Polynomial.aeval (f x)) p`) is equal to applying `f` to the result of `(Polynomial.aeval x) p`. In other words, the process of evaluating a polynomial at an algebraic element and then applying an algebra homomorphism is the same as first applying the algebra homomorphism and then evaluating the polynomial at the result.
More concisely: For any commutative semirings `R`, semirings `A` and `B`, algebra structures over `R` on `A` and `B`, function-like object `F` from `A` to `B`, and an algebra homomorphism class for `F` from `R` to `A` to `B`, the application of a polynomial evaluation and an algebra homomorphism to an element `x` in `A` commutes: `(Polynomial.aeval (f x)) p = (f (Polynomial.aeval x)) p`, where `f` is an algebra homomorphism from `F`, `p` is a polynomial with coefficients in `R`.
|
Polynomial.adjoin_X
theorem Polynomial.adjoin_X : ∀ {R : Type u} [inst : CommSemiring R], Algebra.adjoin R {Polynomial.X} = ⊤
This theorem states that for any commutative semiring `R`, the minimal subalgebra of polynomials over `R` that includes the polynomial variable `X` is equal to the top element of the algebra lattice, indicating it is the largest possible subalgebra. In other words, any polynomial over `R` can be expressed in terms of the indeterminate `X` and elements from `R` itself.
More concisely: For any commutative semiring `R`, the minimal subalgebra of polynomials over `R` containing the indeterminate `X` is the whole algebra.
|
Polynomial.aeval_algebraMap_apply_eq_algebraMap_eval
theorem Polynomial.aeval_algebraMap_apply_eq_algebraMap_eval :
∀ {R : Type u} {A : Type z} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (x : R)
(p : Polynomial R), (Polynomial.aeval ((algebraMap R A) x)) p = (algebraMap R A) (Polynomial.eval x p)
This theorem states that for any commutative semiring `R`, any semiring `A` with an algebra structure over `R`, any element `x` of `R`, and any polynomial `p` over `R`, the algebra homomorphism that arises from evaluating the polynomial `p` at `x` via `Polynomial.aeval` (where `x` is first mapped from `R` to `A` via the `algebraMap`), yields the same result as first evaluating the polynomial `p` at `x` and then mapping the result from `R` to `A` via the `algebraMap`. In mathematical terms, it asserts that for any polynomial $p$ and any scalar $x$ in $R$, $(\text{Polynomial.aeval} \circ \text{algebraMap} \, R \, A)(x)(p)= (\text{algebraMap} \, R \, A)(\text{Polynomial.eval} \, x \, p)$.
More concisely: For any commutative semiring `R`, semiring `A` with an algebra structure over `R`, element `x` of `R`, and polynomial `p` over `R`, the algebra homomorphism of evaluating `p` at `x` via `Polynomial.aeval` and then mapping the result to `A` via `algebraMap` equals mapping `x` to `A` via `algebraMap` and then evaluating `p` at `x` in `R`. In symbols: `(Polynomial.aeval ∘ algebraMap R A) x p = algebraMap R A (Polynomial.eval x p)`.
|
Polynomial.aevalTower_C
theorem Polynomial.aevalTower_C :
∀ {R : Type u} {S : Type v} {A' : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring A']
[inst_2 : CommSemiring S] [inst_3 : Algebra S R] [inst_4 : Algebra S A'] (g : R →ₐ[S] A') (y : A') (x : R),
(Polynomial.aevalTower g y) (Polynomial.C x) = g x
The theorem `Polynomial.aevalTower_C` asserts that for any types `R`, `S`, and `A'` with `CommSemiring` structures and `Algebra` structures on pairs `(S, R)` and `(S, A')`, and given an algebra homomorphism `g` from `R` to `A'` over base ring `S`, a value `y` in `A'` and a constant `x` in `R`, the application of the `Polynomial.aevalTower` function to the constant polynomial `Polynomial.C x` is equal to the application of `g` to `x`. In other words, when evaluating a constant polynomial under the `aevalTower` function, it's the same as using the algebra homomorphism `g` directly on the constant.
More concisely: For any commutative semirings R, S, and A' with algebra structures over S, and given an algebra homomorphism g from R to A' over S, the evaluation of the constant polynomial C(x) under Polynomial.aevalTower is equal to applying g to x.
|