ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>A : Type z<VAR>B : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A ≃ₐ[R] B<GOAL>↑(Polynomial.mapAlgEquiv f) = Polynomial.mapRingHom ↑f
<VAR>R : Type u<VAR>A : Type z<VAR>B : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>C : Type z<VAR>Semiring C<VAR>Algebra R C<VAR>f : A ≃ₐ[R] B<VAR>g : B ≃ₐ[R] C<GOAL>(Polynomial.mapAlgEquiv f).trans (Polynomial.mapAlgEquiv g) = Polynomial.mapAlgEquiv (f.trans g)
<VAR>R : Type u<VAR>CommSemiring R<GOAL>Algebra.adjoin R {Polynomial.X} = ⊤
<VAR>R : Type u<VAR>B : Type u_2<VAR>CommSemiring R<VAR>Semiring B<VAR>Algebra R B<VAR>f g : R[X] →ₐ[R] B<VAR>hX : f Polynomial.X = g Polynomial.X<GOAL>f = g
<VAR>R : Type u<VAR>A : Type z<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>x : A<VAR>p : R[X]<GOAL>(Polynomial.aeval x) p = Polynomial.eval₂ (algebraMap R A) x p
<VAR>R : Type u<VAR>A : Type z<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>x : A<GOAL>(Polynomial.aeval x) 0 = 0
<VAR>R : Type u<VAR>A : Type z<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>x : A<GOAL>(Polynomial.aeval x) Polynomial.X = x
<VAR>R : Type u<VAR>A : Type z<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>x : A<VAR>r : R<GOAL>(Polynomial.aeval x) (Polynomial.C r) = (algebraMap R A) r
<VAR>R : Type u<VAR>A : Type z<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>x : A<VAR>n : ℕ<VAR>r : R<GOAL>(Polynomial.aeval x) ((Polynomial.monomial n) r) = (algebraMap R A) r * x ^ n
<VAR>R : Type u<VAR>A : Type z<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>x : A<VAR>n : ℕ<GOAL>(Polynomial.aeval x) (Polynomial.X ^ n) = x ^ n
<VAR>R : Type u<VAR>A : Type z<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>p q : R[X]<VAR>x : A<GOAL>(Polynomial.aeval x) (p + q) = (Polynomial.aeval x) p + (Polynomial.aeval x) q
<VAR>R : Type u<VAR>A : Type z<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>x : A<GOAL>(Polynomial.aeval x) 1 = 1
<VAR>R : Type u<VAR>A : Type z<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>x : A<VAR>n : ℕ<GOAL>(Polynomial.aeval x) ↑n = ↑n
<VAR>R : Type u<VAR>A : Type z<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>p q : R[X]<VAR>x : A<GOAL>(Polynomial.aeval x) (p * q) = (Polynomial.aeval x) p * (Polynomial.aeval x) q
<VAR>R : Type u<VAR>CommSemiring R<VAR>p q : R[X]<GOAL>p.comp q = (Polynomial.aeval q) p
<VAR>R : Type u<VAR>CommSemiring R<VAR>p q : R[X]<VAR>A : Type u_3<VAR>Semiring A<VAR>Algebra R A<VAR>x : A<GOAL>(Polynomial.aeval x) (p.comp q) = (Polynomial.aeval ((Polynomial.aeval x) q)) p
<VAR>R : Type u<VAR>CommSemiring R<VAR>p q : R[X]<VAR>hpq : p.comp q = Polynomial.X<VAR>hqp : q.comp p = Polynomial.X<VAR>a : R[X]<GOAL>(p.algEquivOfCompEqX q hpq hqp).symm a = (Polynomial.aeval q) a
<VAR>R : Type u<VAR>CommSemiring R<VAR>p q : R[X]<VAR>hpq : p.comp q = Polynomial.X<VAR>hqp : q.comp p = Polynomial.X<VAR>a : R[X]<GOAL>(p.algEquivOfCompEqX q hpq hqp) a = (Polynomial.aeval p) a
<VAR>R : Type u_3<VAR>CommRing R<VAR>t : R<VAR>a : R[X]<GOAL>(Polynomial.algEquivAevalXAddC t).symm a = (Polynomial.aeval (Polynomial.X - Polynomial.C t)) a
<VAR>R : Type u_3<VAR>CommRing R<VAR>t : R<VAR>a : R[X]<GOAL>(Polynomial.algEquivAevalXAddC t) a = (Polynomial.aeval (Polynomial.X + Polynomial.C t)) a
<VAR>R : Type u<VAR>A : Type z<VAR>B : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A →ₐ[R] B<VAR>x : A<GOAL>Polynomial.aeval (f x) = f.comp (Polynomial.aeval x)
<VAR>R : Type u<VAR>CommSemiring R<GOAL>Polynomial.aeval Polynomial.X = AlgHom.id R R[X]
<VAR>R : Type u<VAR>CommSemiring R<VAR>p : R[X]<GOAL>(Polynomial.aeval Polynomial.X) p = p
<VAR>R : Type u<VAR>A : Type z<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>φ : R[X] →ₐ[R] A<VAR>p : R[X]<GOAL>φ p = Polynomial.eval₂ (algebraMap R A) (φ Polynomial.X) p
<VAR>R : Type u<VAR>A : Type z<VAR>B : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>F : Type u_3<VAR>FunLike F A B<VAR>AlgHomClass F R A B<VAR>f : F<VAR>x : A<VAR>p : R[X]<GOAL>(Polynomial.aeval (f x)) p = f ((Polynomial.aeval x) p)
<VAR>R : Type u<VAR>A : Type z<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>p : R[X]<VAR>x : A<VAR>S : Subalgebra R A<VAR>h : x ∈ S<GOAL>↑((Polynomial.aeval ⟨x, h⟩) p) = (Polynomial.aeval x) p
<VAR>R : Type u<VAR>A : Type z<VAR>B : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A ≃ₐ[R] B<VAR>x : A<GOAL>Polynomial.aeval (f x) = (↑f).comp (Polynomial.aeval x)
<VAR>R : Type u<VAR>A : Type z<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>x : R<VAR>p : R[X]<GOAL>(Polynomial.aeval ((algebraMap R A) x)) p = (algebraMap R A) (Polynomial.eval x p)
<VAR>R : Type u<VAR>CommSemiring R<VAR>r : R<GOAL>⇑(Polynomial.aeval r) = Polynomial.eval r
<VAR>R : Type u<VAR>CommSemiring R<VAR>x : R<GOAL>↑(Polynomial.aeval x) = Polynomial.evalRingHom x
<VAR>R : Type u<VAR>CommSemiring R<VAR>X : Type u_3<VAR>g : R[X]<VAR>f : X → R<VAR>x : X<GOAL>(Polynomial.aeval f) g x = (Polynomial.aeval (f x)) g
<VAR>R : Type u<VAR>CommSemiring R<VAR>g : R[X]<VAR>A : Type u_3<VAR>Semiring A<VAR>Algebra R A<VAR>s : Subalgebra R A<VAR>f : ↥s<GOAL>↑((Polynomial.aeval f) g) = (Polynomial.aeval ↑f) g
<VAR>R : Type u<VAR>CommSemiring R<VAR>p : R[X]<GOAL>p.coeff 0 = (Polynomial.aeval 0) p
<VAR>R : Type u<VAR>A : Type z<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>p : R[X]<GOAL>(algebraMap R A) (p.coeff 0) = (Polynomial.aeval 0) p
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Type u_3<VAR>T : Type u_4<VAR>U : Type u_5<VAR>Semiring S<VAR>CommSemiring T<VAR>Semiring U<VAR>Algebra R S<VAR>Algebra T U<VAR>φ : R →+* T<VAR>ψ : S →+* U<VAR>h : (algebraMap T U).comp φ = ψ.comp (algebraMap R S)<VAR>p : R[X]<VAR>a : S<GOAL>ψ ((Polynomial.aeval a) p) = (Polynomial.aeval (ψ a)) (Polynomial.map φ p)
<VAR>S : Type v<VAR>T : Type w<VAR>CommSemiring S<VAR>CommSemiring T<VAR>Algebra S T<VAR>p q : S[X]<VAR>h₁ : p ∣ q<VAR>a : T<VAR>h₂ : (Polynomial.aeval a) p = 0<GOAL>(Polynomial.aeval a) q = 0
<VAR>R : Type u<VAR>A : Type z<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>x : A<GOAL>Algebra.adjoin R {x} = (Polynomial.aeval x).range
<VAR>R : Type u<VAR>A : Type z<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>p : R[X]<VAR>x : A<GOAL>(Polynomial.aeval x) p ∈ Algebra.adjoin R {x}
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>p : R[X]<VAR>x : S<GOAL>(Polynomial.aeval x) p = ∑ i ∈ Finset.range (p.natDegree + 1), p.coeff i • x ^ i
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>p : R[X]<VAR>n : ℕ<VAR>hn : p.natDegree < n<VAR>x : S<GOAL>(Polynomial.aeval x) p = ∑ i ∈ Finset.range n, p.coeff i • x ^ i
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>p : R[X]<VAR>Semiring S<VAR>f : R →+* S<VAR>hf : Function.Injective ⇑f<VAR>r : R<GOAL>Polynomial.eval₂ f (f r) p = 0 → p.IsRoot r
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>p : R[X]<VAR>inj : Function.Injective ⇑(algebraMap R S)<VAR>r : R<VAR>hr : (Polynomial.aeval ((algebraMap R S) r)) p = 0<GOAL>p.IsRoot r
<VAR>R : Type u<VAR>S : Type v<VAR>A' : Type u_1<VAR>CommSemiring R<VAR>CommSemiring A'<VAR>CommSemiring S<VAR>Algebra S R<VAR>Algebra S A'<VAR>g : R →ₐ[S] A'<VAR>y : A'<GOAL>(Polynomial.aevalTower g y) Polynomial.X = y
<VAR>R : Type u<VAR>S : Type v<VAR>A' : Type u_1<VAR>CommSemiring R<VAR>CommSemiring A'<VAR>CommSemiring S<VAR>Algebra S R<VAR>Algebra S A'<VAR>g : R →ₐ[S] A'<VAR>y : A'<VAR>x : R<GOAL>(Polynomial.aevalTower g y) (Polynomial.C x) = g x
<VAR>R : Type u<VAR>S : Type v<VAR>A' : Type u_1<VAR>CommSemiring R<VAR>CommSemiring A'<VAR>CommSemiring S<VAR>Algebra S R<VAR>Algebra S A'<VAR>g : R →ₐ[S] A'<VAR>y : A'<GOAL>(↑(Polynomial.aevalTower g y)).comp Polynomial.C = ↑g
<VAR>R : Type u<VAR>S : Type v<VAR>A' : Type u_1<VAR>CommSemiring R<VAR>CommSemiring A'<VAR>CommSemiring S<VAR>Algebra S R<VAR>Algebra S A'<VAR>g : R →ₐ[S] A'<VAR>y : A'<VAR>x : R<GOAL>(Polynomial.aevalTower g y) ((algebraMap R R[X]) x) = g x
<VAR>R : Type u<VAR>S : Type v<VAR>A' : Type u_1<VAR>CommSemiring R<VAR>CommSemiring A'<VAR>CommSemiring S<VAR>Algebra S R<VAR>Algebra S A'<VAR>g : R →ₐ[S] A'<VAR>y : A'<GOAL>(↑(Polynomial.aevalTower g y)).comp (algebraMap R R[X]) = ↑g
<VAR>R : Type u<VAR>S : Type v<VAR>A' : Type u_1<VAR>CommSemiring R<VAR>CommSemiring A'<VAR>CommSemiring S<VAR>Algebra S R<VAR>Algebra S A'<VAR>g : R →ₐ[S] A'<VAR>y : A'<VAR>x : R<GOAL>(Polynomial.aevalTower g y) ((IsScalarTower.toAlgHom S R R[X]) x) = g x
<VAR>R : Type u<VAR>S : Type v<VAR>A' : Type u_1<VAR>CommSemiring R<VAR>CommSemiring A'<VAR>CommSemiring S<VAR>Algebra S R<VAR>Algebra S A'<VAR>g : R →ₐ[S] A'<VAR>y : A'<GOAL>(Polynomial.aevalTower g y).comp (IsScalarTower.toAlgHom S R R[X]) = g
<VAR>S : Type v<VAR>CommSemiring S<GOAL>Polynomial.aevalTower (AlgHom.id S S) = Polynomial.aeval
<VAR>S : Type v<VAR>A' : Type u_1<VAR>CommSemiring A'<VAR>CommSemiring S<VAR>Algebra S A'<GOAL>Polynomial.aevalTower (Algebra.ofId S A') = Polynomial.aeval
<VAR>S : Type v<VAR>CommRing S<VAR>z p : S<VAR>f : S[X]<VAR>i : ℕ<VAR>dvd_eval : p ∣ Polynomial.eval z f<VAR>dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ f.coeff j * z ^ j<GOAL>p ∣ f.coeff i * z ^ i
<VAR>S : Type v<VAR>CommRing S<VAR>r p : S<VAR>f : S[X]<VAR>i : ℕ<VAR>hr : f.IsRoot r<VAR>h : ∀ (j : ℕ), j ≠ i → p ∣ f.coeff j * r ^ j<GOAL>p ∣ f.coeff i * r ^ i
<VAR>R : Type u<VAR>Ring R<VAR>p : R[X]<VAR>r : R<GOAL>Polynomial.eval r (p * (Polynomial.X - Polynomial.C r)) = 0
<VAR>R : Type u<VAR>Ring R<VAR>Nontrivial R<VAR>r : R<GOAL>¬IsUnit (Polynomial.X - Polynomial.C r)
<VAR>R : Type u<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>f : M →ₗ[R] M<VAR>v : M<VAR>p : R[X]<GOAL>((Polynomial.aeval f) p) v = p.sum fun n b => b • (f ^ n) v
<VAR>R : Type u<VAR>A : Type z<VAR>M : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>q : Submodule R M<VAR>m : M<VAR>hm : m ∈ q<VAR>p : R[X]<VAR>Semiring A<VAR>Algebra R A<VAR>Module A M<VAR>IsScalarTower R A M<VAR>a : A<VAR>hq : q ≤ Submodule.comap ((Algebra.lsmul R R M) a) q<GOAL>(Polynomial.aeval a) p • m ∈ q
<VAR>R : Type u<VAR>M : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>q : Submodule R M<VAR>m : M<VAR>hm : m ∈ q<VAR>p : R[X]<VAR>f : Module.End R M<VAR>hq : q ≤ Submodule.comap f q<GOAL>((Polynomial.aeval f) p) m ∈ q
<VAR>R : Type u<VAR>Semiring R<VAR>Nontrivial R<VAR>i j : ℕ<GOAL>(Polynomial.monomial i) 1 = (Polynomial.monomial j) 1 ↔ i = j
<VAR>R : Type u<VAR>Semiring R<VAR>f : Polynomial R<GOAL>f.support.card ≤ 1 ↔ ∃ n a, f = (Polynomial.monomial n) a
<VAR>R : Type u<VAR>Semiring R<VAR>S : Type u_1<VAR>Semiring S<VAR>f g : Polynomial R →+* S<VAR>h₁ : ∀ (a : R), f (Polynomial.C a) = g (Polynomial.C a)<VAR>h₂ : f Polynomial.X = g Polynomial.X<GOAL>f = g
<VAR>R : Type u<VAR>Semiring R<VAR>S : Type u_1<VAR>Semiring S<VAR>f g : Polynomial R →+* S<VAR>h₁ : f.comp Polynomial.C = g.comp Polynomial.C<VAR>h₂ : f Polynomial.X = g Polynomial.X<GOAL>f = g
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>p : Polynomial R<VAR>hp : p.Monic<VAR>hp2 : 2 ≤ p.natDegree<VAR>hp3 : p.natDegree ≤ 3<GOAL>Irreducible p ↔ p.roots = 0
<VAR>K : Type u_1<VAR>Field K<VAR>p : Polynomial K<VAR>hp2 : 2 ≤ p.natDegree<VAR>hp3 : p.natDegree ≤ 3<GOAL>Irreducible p ↔ p.roots = 0
<VAR>S : Type u_1<VAR>Semiring S<VAR>l : List S[X]<GOAL>l.sum.natDegree ≤ List.foldr max 0 (List.map Polynomial.natDegree l)
<VAR>S : Type u_1<VAR>Semiring S<VAR>l : Multiset S[X]<GOAL>l.sum.natDegree ≤ Multiset.foldr max ⋯ 0 (Multiset.map Polynomial.natDegree l)
<VAR>ι : Type w<VAR>s : Finset ι<VAR>S : Type u_1<VAR>Semiring S<VAR>f : ι → S[X]<GOAL>(∑ i ∈ s, f i).natDegree ≤ Finset.fold max 0 (Polynomial.natDegree ∘ f) s
<VAR>ι : Type w<VAR>s : Finset ι<VAR>S : Type u_1<VAR>Semiring S<VAR>n : ℕ<VAR>f : ι → S[X]<VAR>h : ∀ i ∈ s, (f i).natDegree ≤ n<GOAL>(∑ i ∈ s, f i).natDegree ≤ n
<VAR>S : Type u_1<VAR>Semiring S<VAR>l : List S[X]<GOAL>l.sum.degree ≤ (List.map Polynomial.natDegree l).maximum
<VAR>S : Type u_1<VAR>Semiring S<VAR>l : List S[X]<GOAL>l.prod.natDegree ≤ (List.map Polynomial.natDegree l).sum
<VAR>S : Type u_1<VAR>Semiring S<VAR>l : List S[X]<GOAL>l.prod.degree ≤ (List.map Polynomial.degree l).sum
<VAR>S : Type u_1<VAR>Semiring S<VAR>l : List S[X]<VAR>n : ℕ<VAR>hl : ∀ p ∈ l, p.natDegree ≤ n<GOAL>l.prod.coeff (l.length * n) = (List.map (fun p => p.coeff n) l).prod
<VAR>R : Type u<VAR>CommSemiring R<VAR>t : Multiset R[X]<GOAL>t.prod.natDegree ≤ (Multiset.map Polynomial.natDegree t).sum
<VAR>R : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>CommSemiring R<VAR>f : ι → R[X]<GOAL>(∏ i ∈ s, f i).natDegree ≤ ∑ i ∈ s, (f i).natDegree
<VAR>R : Type u<VAR>CommSemiring R<VAR>t : Multiset R[X]<GOAL>t.prod.degree ≤ (Multiset.map Polynomial.degree t).sum
<VAR>R : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>CommSemiring R<VAR>f : ι → R[X]<GOAL>(∏ i ∈ s, f i).degree ≤ ∑ i ∈ s, (f i).degree
<VAR>R : Type u<VAR>CommSemiring R<VAR>t : Multiset R[X]<VAR>h : (Multiset.map Polynomial.leadingCoeff t).prod ≠ 0<GOAL>t.prod.leadingCoeff = (Multiset.map Polynomial.leadingCoeff t).prod
<VAR>R : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>CommSemiring R<VAR>f : ι → R[X]<VAR>h : ∏ i ∈ s, (f i).leadingCoeff ≠ 0<GOAL>(∏ i ∈ s, f i).leadingCoeff = ∏ i ∈ s, (f i).leadingCoeff
<VAR>R : Type u<VAR>CommSemiring R<VAR>t : Multiset R[X]<VAR>h : (Multiset.map (fun f => f.leadingCoeff) t).prod ≠ 0<GOAL>t.prod.natDegree = (Multiset.map (fun f => f.natDegree) t).sum
<VAR>R : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>CommSemiring R<VAR>f : ι → R[X]<VAR>h : ∏ i ∈ s, (f i).leadingCoeff ≠ 0<GOAL>(∏ i ∈ s, f i).natDegree = ∑ i ∈ s, (f i).natDegree
<VAR>R : Type u<VAR>CommSemiring R<VAR>t : Multiset R[X]<VAR>h : ∀ f ∈ t, f.Monic<GOAL>t.prod.natDegree = (Multiset.map Polynomial.natDegree t).sum
<VAR>R : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>CommSemiring R<VAR>f : ι → R[X]<VAR>h : ∀ i ∈ s, (f i).Monic<GOAL>(∏ i ∈ s, f i).natDegree = ∑ i ∈ s, (f i).natDegree
<VAR>R : Type u<VAR>CommSemiring R<VAR>t : Multiset R[X]<VAR>n : ℕ<VAR>hl : ∀ p ∈ t, p.natDegree ≤ n<GOAL>t.prod.coeff (Multiset.card t * n) = (Multiset.map (fun p => p.coeff n) t).prod
<VAR>R : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>CommSemiring R<VAR>f : ι → R[X]<VAR>n : ℕ<VAR>h : ∀ p ∈ s, (f p).natDegree ≤ n<GOAL>(∏ i ∈ s, f i).coeff (s.card * n) = ∏ i ∈ s, (f i).coeff n
<VAR>R : Type u<VAR>CommSemiring R<VAR>t : Multiset R[X]<GOAL>t.prod.coeff 0 = (Multiset.map (fun f => f.coeff 0) t).prod
<VAR>R : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>CommSemiring R<VAR>f : ι → R[X]<GOAL>(∏ i ∈ s, f i).coeff 0 = ∏ i ∈ s, (f i).coeff 0
<VAR>R : Type u<VAR>CommRing R<VAR>t : Multiset R<GOAL>(Multiset.map (fun x => Polynomial.X - Polynomial.C x) t).prod.nextCoeff = -t.sum
<VAR>R : Type u<VAR>ι : Type w<VAR>CommRing R<VAR>s : Finset ι<VAR>f : ι → R<GOAL>(∏ i ∈ s, (Polynomial.X - Polynomial.C (f i))).nextCoeff = -∑ i ∈ s, f i
<VAR>R : Type u<VAR>CommRing R<VAR>t : Multiset R<VAR>ht : 0 < Multiset.card t<GOAL>(Multiset.map (fun x => Polynomial.X - Polynomial.C x) t).prod.coeff (Multiset.card t - 1) = -t.sum
<VAR>R : Type u<VAR>ι : Type w<VAR>CommRing R<VAR>s : Finset ι<VAR>f : ι → R<VAR>hs : 0 < s.card<GOAL>(∏ i ∈ s, (Polynomial.X - Polynomial.C (f i))).coeff (s.card - 1) = -∑ i ∈ s, f i
<VAR>R : Type u<VAR>Semiring R<VAR>NoZeroDivisors R<VAR>Nontrivial R<VAR>l : List R[X]<GOAL>l.prod.degree = (List.map Polynomial.degree l).sum
<VAR>R : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>CommSemiring R<VAR>NoZeroDivisors R<VAR>f : ι → R[X]<VAR>h : ∀ i ∈ s, f i ≠ 0<GOAL>(∏ i ∈ s, f i).natDegree = ∑ i ∈ s, (f i).natDegree
<VAR>R : Type u<VAR>CommSemiring R<VAR>NoZeroDivisors R<VAR>t : Multiset R[X]<VAR>h : 0 ∉ t<GOAL>t.prod.natDegree = (Multiset.map Polynomial.natDegree t).sum
<VAR>R : Type u<VAR>CommSemiring R<VAR>NoZeroDivisors R<VAR>t : Multiset R[X]<VAR>Nontrivial R<GOAL>t.prod.degree = (Multiset.map (fun f => f.degree) t).sum
<VAR>R : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>CommSemiring R<VAR>NoZeroDivisors R<VAR>f : ι → R[X]<VAR>Nontrivial R<GOAL>(∏ i ∈ s, f i).degree = ∑ i ∈ s, (f i).degree
<VAR>R : Type u<VAR>CommSemiring R<VAR>NoZeroDivisors R<VAR>t : Multiset R[X]<GOAL>t.prod.leadingCoeff = (Multiset.map (fun f => f.leadingCoeff) t).prod
<VAR>R : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>CommSemiring R<VAR>NoZeroDivisors R<VAR>f : ι → R[X]<GOAL>(∏ i ∈ s, f i).leadingCoeff = ∏ i ∈ s, (f i).leadingCoeff
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>a : Polynomial R<GOAL>Polynomial.derivative' a = Polynomial.derivative a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>Module (Polynomial R) A<VAR>D : Derivation R (Polynomial R) A<VAR>a : R<GOAL>D (Polynomial.C a) = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>Module (Polynomial R) A<VAR>D : Derivation R (Polynomial R) A<VAR>a : R<VAR>f : Polynomial R<GOAL>Polynomial.C a • D f = a • D f
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>Module (Polynomial R) A<VAR>D₁ D₂ : Derivation R (Polynomial R) A<VAR>h : D₁ Polynomial.X = D₂ Polynomial.X<GOAL>D₁ = D₂
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>Module (Polynomial R) A<VAR>IsScalarTower R (Polynomial R) A<VAR>a : A<VAR>f : Polynomial R<GOAL>((Polynomial.mkDerivation R) a) f = Polynomial.derivative f • a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>Module (Polynomial R) A<VAR>IsScalarTower R (Polynomial R) A<VAR>a : A<GOAL>((Polynomial.mkDerivation R) a) Polynomial.X = a
<VAR>R : Type u_1<VAR>CommSemiring R<GOAL>(Polynomial.mkDerivation R) 1 = Polynomial.derivative'
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>f : Polynomial R<GOAL>((Polynomial.mkDerivation R) 1) f = Polynomial.derivative f
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>Module (Polynomial R) A<VAR>IsScalarTower R (Polynomial R) A<VAR>a : A<GOAL>(Polynomial.mkDerivationEquiv R) a = (Polynomial.mkDerivation R) a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>Module (Polynomial R) A<VAR>IsScalarTower R (Polynomial R) A<VAR>D : Derivation R (Polynomial R) A<GOAL>(Polynomial.mkDerivationEquiv R).symm D = D Polynomial.X
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_3<VAR>CommSemiring R<VAR>CommSemiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module A M<VAR>Module R M<VAR>IsScalarTower R A M<VAR>d : Derivation R A M<VAR>a : A<VAR>f : Polynomial R<GOAL>(d.compAEval a) f = (Module.AEval.of R M a) (d ((Polynomial.aeval a) f))
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_3<VAR>CommSemiring R<VAR>CommSemiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module A M<VAR>Module R M<VAR>IsScalarTower R A M<VAR>a : A<VAR>d : Derivation R A M<VAR>f : Polynomial R<GOAL>(d.compAEval a) f = Polynomial.derivative f • (Module.AEval.of R M a) (d a)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_3<VAR>CommSemiring R<VAR>CommSemiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module A M<VAR>Module R M<VAR>IsScalarTower R A M<VAR>a : A<VAR>d : Derivation R A M<VAR>f : Polynomial R<GOAL>d ((Polynomial.aeval a) f) = (Polynomial.aeval a) (Polynomial.derivative f) • d a
<VAR>R : Type u_3<VAR>Semiring R<VAR>p : Polynomial R<VAR>S : Type u_4<VAR>AddCommMonoid S<VAR>Pow S ℕ<VAR>MulActionWithZero R S<VAR>x : S<GOAL>p.smeval x = p.sum (Polynomial.smul_pow x)
<VAR>R : Type u_1<VAR>Semiring R<VAR>p : Polynomial R<VAR>S : Type u_2<VAR>AddCommMonoid S<VAR>Pow S ℕ<VAR>MulActionWithZero R S<VAR>x : S<GOAL>p.smeval x = p.sum (Polynomial.smul_pow x)
<VAR>R : Type u_1<VAR>Semiring R<VAR>r : R<VAR>S : Type u_2<VAR>AddCommMonoid S<VAR>Pow S ℕ<VAR>MulActionWithZero R S<VAR>x : S<GOAL>(Polynomial.C r).smeval x = r • x ^ 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>r : R<VAR>S : Type u_2<VAR>AddCommMonoid S<VAR>Pow S ℕ<VAR>MulActionWithZero R S<VAR>x : S<VAR>n : ℕ<GOAL>((Polynomial.monomial n) r).smeval x = r • x ^ n
<VAR>R : Type u_1<VAR>Semiring R<VAR>r : R<VAR>p : Polynomial R<GOAL>Polynomial.eval r p = p.smeval r
<VAR>R : Type u_3<VAR>Semiring R<VAR>S : Type u_4<VAR>Semiring S<VAR>f : R →+* S<VAR>p : Polynomial R<VAR>x : S<GOAL>Polynomial.eval₂ f x p = p.smeval x
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Type u_2<VAR>AddCommMonoid S<VAR>Pow S ℕ<VAR>MulActionWithZero R S<VAR>x : S<GOAL>Polynomial.smeval 0 x = 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Type u_2<VAR>AddCommMonoid S<VAR>Pow S ℕ<VAR>MulActionWithZero R S<VAR>x : S<GOAL>Polynomial.smeval 1 x = 1 • x ^ 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Type u_2<VAR>AddCommMonoid S<VAR>Pow S ℕ<VAR>MulActionWithZero R S<VAR>x : S<GOAL>Polynomial.X.smeval x = x ^ 1
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Type u_2<VAR>AddCommMonoid S<VAR>Pow S ℕ<VAR>MulActionWithZero R S<VAR>x : S<VAR>n : ℕ<GOAL>(Polynomial.X ^ n).smeval x = x ^ n
<VAR>R : Type u_1<VAR>Semiring R<VAR>p q : Polynomial R<VAR>S : Type u_2<VAR>AddCommMonoid S<VAR>Pow S ℕ<VAR>Module R S<VAR>x : S<GOAL>(p + q).smeval x = p.smeval x + q.smeval x
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Type u_2<VAR>AddCommMonoid S<VAR>Pow S ℕ<VAR>Module R S<VAR>x : S<VAR>n : ℕ<GOAL>(↑n).smeval x = n • x ^ 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>p : Polynomial R<VAR>S : Type u_2<VAR>AddCommMonoid S<VAR>Pow S ℕ<VAR>Module R S<VAR>x : S<VAR>r : R<GOAL>(r • p).smeval x = r • p.smeval x
<VAR>R : Type u_1<VAR>Semiring R<VAR>p : Polynomial R<VAR>S : Type u_2<VAR>AddCommMonoid S<VAR>Pow S ℕ<VAR>Module R S<VAR>x : S<GOAL>(Polynomial.smeval.linearMap R x) p = p.smeval x
<VAR>R : Type u_3<VAR>Semiring R<VAR>r : R<GOAL>⇑(Polynomial.leval r) = fun p => p.smeval r
<VAR>R : Type u_3<VAR>Semiring R<VAR>r : R<GOAL>Polynomial.leval r = Polynomial.smeval.linearMap R r
<VAR>R : Type u_1<VAR>Ring R<VAR>S : Type u_2<VAR>AddCommGroup S<VAR>Pow S ℕ<VAR>Module R S<VAR>p : Polynomial R<VAR>x : S<GOAL>(-p).smeval x = -p.smeval x
<VAR>R : Type u_1<VAR>Ring R<VAR>S : Type u_2<VAR>AddCommGroup S<VAR>Pow S ℕ<VAR>Module R S<VAR>p q : Polynomial R<VAR>x : S<GOAL>(p - q).smeval x = p.smeval x - q.smeval x
<VAR>S : Type u_3<VAR>NonAssocRing S<VAR>Pow S ℕ<VAR>NatPowAssoc S<VAR>q : Polynomial ℕ<VAR>n : ℕ<GOAL>q.smeval (-↑n) = ↑(q.smeval (-↑n))
<VAR>S : Type u_2<VAR>NonAssocSemiring S<VAR>Pow S ℕ<VAR>NatPowAssoc S<VAR>q : Polynomial ℕ<VAR>n : ℕ<GOAL>q.smeval ↑n = ↑(q.smeval n)
<VAR>R : Type u_1<VAR>Semiring R<VAR>p : Polynomial R<VAR>S : Type u_2<VAR>NonAssocSemiring S<VAR>Module R S<VAR>Pow S ℕ<VAR>NatPowAssoc S<GOAL>p.smeval 0 = p.coeff 0 • 1
<VAR>R : Type u_1<VAR>Semiring R<VAR>p : Polynomial R<VAR>S : Type u_2<VAR>NonAssocSemiring S<VAR>Module R S<VAR>IsScalarTower R S S<VAR>Pow S ℕ<VAR>NatPowAssoc S<VAR>x : S<GOAL>(p * Polynomial.X).smeval x = p.smeval x * x
<VAR>R : Type u_1<VAR>Semiring R<VAR>p : Polynomial R<VAR>S : Type u_2<VAR>NonAssocSemiring S<VAR>Module R S<VAR>SMulCommClass R S S<VAR>Pow S ℕ<VAR>NatPowAssoc S<VAR>x : S<GOAL>(Polynomial.X * p).smeval x = x * p.smeval x
<VAR>R : Type u_1<VAR>Semiring R<VAR>p : Polynomial R<VAR>S : Type u_2<VAR>NonAssocSemiring S<VAR>Module R S<VAR>IsScalarTower R S S<VAR>Pow S ℕ<VAR>NatPowAssoc S<VAR>x : S<VAR>m n : ℕ<GOAL>p.smeval x * x ^ m * x ^ n = p.smeval x * (x ^ m * x ^ n)
<VAR>R : Type u_1<VAR>Semiring R<VAR>p : Polynomial R<VAR>S : Type u_2<VAR>NonAssocSemiring S<VAR>Module R S<VAR>IsScalarTower R S S<VAR>Pow S ℕ<VAR>NatPowAssoc S<VAR>x : S<VAR>n : ℕ<GOAL>(p * Polynomial.X ^ n).smeval x = p.smeval x * x ^ n
<VAR>R : Type u_1<VAR>Semiring R<VAR>p : Polynomial R<VAR>S : Type u_2<VAR>NonAssocSemiring S<VAR>Module R S<VAR>SMulCommClass R S S<VAR>Pow S ℕ<VAR>NatPowAssoc S<VAR>x : S<VAR>m n : ℕ<GOAL>x ^ m * x ^ n * p.smeval x = x ^ m * (x ^ n * p.smeval x)
<VAR>R : Type u_1<VAR>Semiring R<VAR>p : Polynomial R<VAR>S : Type u_2<VAR>NonAssocSemiring S<VAR>Module R S<VAR>SMulCommClass R S S<VAR>Pow S ℕ<VAR>NatPowAssoc S<VAR>x : S<VAR>n : ℕ<GOAL>(Polynomial.X ^ n * p).smeval x = x ^ n * p.smeval x
<VAR>R : Type u_1<VAR>Semiring R<VAR>r : R<VAR>p : Polynomial R<VAR>S : Type u_2<VAR>NonAssocSemiring S<VAR>Module R S<VAR>Pow S ℕ<VAR>x : S<GOAL>(Polynomial.C r * p).smeval x = r • p.smeval x