MvPolynomial.eval₂Hom_X
theorem MvPolynomial.eval₂Hom_X :
∀ {S : Type v} [inst : CommRing S] {R : Type u} (c : ℤ →+* S) (f : MvPolynomial R ℤ →+* S) (x : MvPolynomial R ℤ),
MvPolynomial.eval₂ c (⇑f ∘ MvPolynomial.X) x = f x
This theorem is about multivariate polynomials and ring homomorphisms. Specifically, it states that a ring homomorphism `f` from the ring of integer-coefficient multivariate polynomials `Z[X_1, X_2, ...]` to any commutative ring `R` is completely determined by the evaluations of the polynomial variables `X_1, X_2, ...` under `f`. In other words, for any multivariate polynomial `x`, the evaluation of `x` under the ring homomorphism `f` is equal to the evaluation of `x` under the function that first applies the polynomial variable mapping `MvPolynomial.X` and then applies `f`. The mapping `c` is a ring homomorphism from the integers to `S`, where `S` is a type with a commutative ring structure.
More concisely: A ring homomorphism from the ring of multivariate polynomials over integers to any commutative ring is uniquely determined by its action on polynomial variables.
|
MvPolynomial.eval_sub
theorem MvPolynomial.eval_sub :
∀ {R : Type u} {σ : Type u_1} [inst : CommRing R] (p : MvPolynomial σ R) {q : MvPolynomial σ R} (f : σ → R),
(MvPolynomial.eval f) (p - q) = (MvPolynomial.eval f) p - (MvPolynomial.eval f) q
The theorem `MvPolynomial.eval_sub` states that for any commutative ring `R` and any type `σ`, given any two multivariate polynomials `p` and `q` over the ring `R` with variables indexed by `σ`, and a valuation `f` of the variables, the result of evaluating the difference of `p` and `q` under valuation `f` is equal to the difference of the evaluation of `p` and the evaluation of `q` under the same valuation. In other words, it asserts the compatibility of evaluation with subtraction in the context of multivariate polynomials.
More concisely: For any commutative ring R and type σ, given multivariate polynomials p and q over R indexed by σ, and a valuation f of the variables, the evaluation of p - q under f equals the evaluation of p under f - the evaluation of q under f.
|