-
-
Save jcommelin/0e401d47ac3e0b7291c27d3313ea850f to your computer and use it in GitHub Desktop.
Evaluation of polynomials is associative
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
import linear_algebra.multivariate_polynomial | |
universes u v w | |
variables {σ : Type v} [decidable_eq σ] | |
variables {R : Type u} [decidable_eq R] [comm_ring R] | |
variables {τ : Type w} [decidable_eq τ] | |
open mv_polynomial | |
theorem eval_assoc₁ | |
(f : mv_polynomial σ R) (g : σ → mv_polynomial τ R) (h : τ → R) | |
: f.eval (λ n : σ, (g n).eval h) = ((functorial C f).eval g).eval h := | |
begin | |
sorry | |
end | |
theorem eval_assoc₂ | |
(f : mv_polynomial σ (mv_polynomial τ R)) (g : σ → mv_polynomial τ R) (h : τ → R) | |
: C ((f.eval g).eval h) = f.eval (λ n : σ, C ((g n).eval h)) := | |
begin | |
sorry | |
end |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment