ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>x : S<VAR>p : R[ℕ]<GOAL>Polynomial.eval₂ f x { toFinsupp := p } = (AddMonoidAlgebra.liftNC ↑f ⇑((powersHom S) x)) p
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>p q : R[X]<VAR>Semiring S<VAR>f : R →+* S<VAR>x : S<VAR>hf : ∀ (k : ℕ), Commute (f (q.coeff k)) x<GOAL>Polynomial.eval₂ f x (p * q) = Polynomial.eval₂ f x p * Polynomial.eval₂ f x q
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>p : R[X]<VAR>Semiring S<VAR>f : R →+* S<VAR>x : S<GOAL>Polynomial.eval₂ f x (p * Polynomial.X) = Polynomial.eval₂ f x p * x
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>p : R[X]<VAR>Semiring S<VAR>f : R →+* S<VAR>x : S<GOAL>Polynomial.eval₂ f x (Polynomial.X * p) = Polynomial.eval₂ f x p * x
<VAR>R : Type u<VAR>S : Type v<VAR>a : R<VAR>Semiring R<VAR>p : R[X]<VAR>Semiring S<VAR>f : R →+* S<VAR>x : S<VAR>h : Commute (f a) x<GOAL>Polynomial.eval₂ f x (p * Polynomial.C a) = Polynomial.eval₂ f x p * f a
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>x : S<VAR>ps : List R[X]<VAR>hf : ∀ p ∈ ps, ∀ (k : ℕ), Commute (f (p.coeff k)) x<GOAL>Polynomial.eval₂ f x ps.prod = (List.map (Polynomial.eval₂ f x) ps).prod
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>x : S<VAR>hf : ∀ (a : R), Commute (f a) x<VAR>p : R[X]<GOAL>(Polynomial.eval₂RingHom' f x hf) p = Polynomial.eval₂ f x p
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>p : R[X]<VAR>Semiring S<VAR>f : R →+* S<VAR>x : S<GOAL>Polynomial.eval₂ f x p = ∑ i ∈ Finset.range (p.natDegree + 1), f (p.coeff i) * x ^ i
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>p : R[X]<VAR>n : ℕ<VAR>hn : p.natDegree < n<VAR>x : S<GOAL>Polynomial.eval₂ f x p = ∑ i ∈ Finset.range n, f (p.coeff i) * x ^ i
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>p q : R[X]<VAR>CommSemiring S<VAR>f : R →+* S<VAR>x : S<GOAL>Polynomial.eval₂ f x (p * q) = Polynomial.eval₂ f x p * Polynomial.eval₂ f x q
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>p : R[X]<VAR>CommSemiring S<VAR>f : R →+* S<VAR>x : S<VAR>q : R[X]<VAR>hp : Polynomial.eval₂ f x p = 0<GOAL>Polynomial.eval₂ f x (p * q) = 0
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>q : R[X]<VAR>CommSemiring S<VAR>f : R →+* S<VAR>x : S<VAR>p : R[X]<VAR>hq : Polynomial.eval₂ f x q = 0<GOAL>Polynomial.eval₂ f x (p * q) = 0
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>CommSemiring S<VAR>f : R →+* S<VAR>x : S<GOAL>⇑(Polynomial.eval₂RingHom f x) = Polynomial.eval₂ f x
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>p : R[X]<VAR>CommSemiring S<VAR>f : R →+* S<VAR>x : S<VAR>n : ℕ<GOAL>Polynomial.eval₂ f x (p ^ n) = Polynomial.eval₂ f x p ^ n
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>p q : R[X]<VAR>CommSemiring S<VAR>f : R →+* S<VAR>x : S<GOAL>p ∣ q → Polynomial.eval₂ f x p ∣ Polynomial.eval₂ f x q
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>p q : R[X]<VAR>CommSemiring S<VAR>f : R →+* S<VAR>x : S<VAR>h : p ∣ q<VAR>h0 : Polynomial.eval₂ f x p = 0<GOAL>Polynomial.eval₂ f x q = 0
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>CommSemiring S<VAR>f : R →+* S<VAR>l : List R[X]<VAR>x : S<GOAL>Polynomial.eval₂ f x l.prod = (List.map (Polynomial.eval₂ f x) l).prod
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>x : R<GOAL>Polynomial.eval x p = p.sum fun e a => a * x ^ e
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>x : R<GOAL>Polynomial.eval x p = ∑ i ∈ Finset.range (p.natDegree + 1), p.coeff i * x ^ i
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ<VAR>hn : p.natDegree < n<VAR>x : R<GOAL>Polynomial.eval x p = ∑ i ∈ Finset.range n, p.coeff i * x ^ i
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>S : Type u_1<VAR>Semiring S<VAR>f : R →+* S<VAR>r : R<GOAL>Polynomial.eval₂ f (f r) p = f (Polynomial.eval r p)
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>S : Type u_1<VAR>Semiring S<VAR>f : R →+* S<GOAL>Polynomial.eval₂ f 1 p = f (Polynomial.eval 1 p)
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>S : Type u_1<VAR>Semiring S<VAR>f : R →+* S<VAR>n : ℕ<GOAL>Polynomial.eval₂ f (↑n) p = f (Polynomial.eval (↑n) p)
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>S : Type u_1<VAR>Semiring S<VAR>f : R →+* S<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>Polynomial.eval₂ f (OfNat.ofNat n) p = f (Polynomial.eval (OfNat.ofNat n) p)
<VAR>R : Type u<VAR>a : R<VAR>Semiring R<VAR>x : R<GOAL>Polynomial.eval x (Polynomial.C a) = a
<VAR>R : Type u<VAR>Semiring R<VAR>x : R<VAR>n : ℕ<GOAL>Polynomial.eval x ↑n = ↑n
<VAR>R : Type u<VAR>Semiring R<VAR>n : ℕ<VAR>n.AtLeastTwo<VAR>a : R<GOAL>Polynomial.eval a (OfNat.ofNat n) = OfNat.ofNat n
<VAR>R : Type u<VAR>Semiring R<VAR>x : R<GOAL>Polynomial.eval x Polynomial.X = x
<VAR>R : Type u<VAR>Semiring R<VAR>x : R<VAR>n : ℕ<VAR>a : R<GOAL>Polynomial.eval x ((Polynomial.monomial n) a) = a * x ^ n
<VAR>R : Type u<VAR>Semiring R<VAR>x : R<GOAL>Polynomial.eval x 0 = 0
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<VAR>x : R<GOAL>Polynomial.eval x (p + q) = Polynomial.eval x p + Polynomial.eval x q
<VAR>R : Type u<VAR>Semiring R<VAR>x : R<GOAL>Polynomial.eval x 1 = 1
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Monoid S<VAR>DistribMulAction S R<VAR>IsScalarTower S R R<VAR>s : S<VAR>p : R[X]<VAR>x : R<GOAL>Polynomial.eval x (s • p) = s • Polynomial.eval x p
<VAR>R : Type u<VAR>a : R<VAR>Semiring R<VAR>p : R[X]<VAR>x : R<GOAL>Polynomial.eval x (Polynomial.C a * p) = a * Polynomial.eval x p
<VAR>S : Type v<VAR>CommRing S<VAR>d : ℕ<VAR>y : S<GOAL>Polynomial.eval (1 + y) ((Polynomial.monomial d) (↑d + 1)) - Polynomial.eval y ((Polynomial.monomial d) (↑d + 1)) = ∑ x_1 ∈ Finset.range (d + 1), ↑((d + 1).choose x_1) * (↑x_1 * y ^ (x_1 - 1))
<VAR>R : Type u_1<VAR>Semiring R<VAR>r : R<VAR>f : R[X]<GOAL>(Polynomial.leval r) f = Polynomial.eval r f
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>x : R<VAR>n : ℕ<GOAL>Polynomial.eval x (↑n * p) = ↑n * Polynomial.eval x p
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>x : R<GOAL>Polynomial.eval x (p * Polynomial.X) = Polynomial.eval x p * x
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>x : R<VAR>k : ℕ<GOAL>Polynomial.eval x (p * Polynomial.X ^ k) = Polynomial.eval x p * x ^ k
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>f : ℕ → R → R[X]<VAR>x : R<GOAL>Polynomial.eval x (p.sum f) = p.sum fun n a => Polynomial.eval x (f n a)
<VAR>R : Type u<VAR>ι : Type y<VAR>Semiring R<VAR>s : Finset ι<VAR>g : ι → R[X]<VAR>x : R<GOAL>Polynomial.eval x (∑ i ∈ s, g i) = ∑ i ∈ s, Polynomial.eval x (g i)
<VAR>R : Type u<VAR>a : R<VAR>Semiring R<VAR>p : R[X]<GOAL>p.IsRoot a ↔ Polynomial.eval a p = 0
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>x : R<VAR>h : p.IsRoot x<GOAL>Polynomial.eval x p = 0
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>p.coeff 0 = Polynomial.eval 0 p
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>hp : p.coeff 0 = 0<GOAL>p.IsRoot 0
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>p q : R[X]<VAR>x : R<VAR>h : p.IsRoot x<VAR>hpq : p ∣ q<GOAL>q.IsRoot x
<VAR>R : Type u<VAR>Semiring R<VAR>r a : R<VAR>hr : r ≠ 0<GOAL>¬(Polynomial.C r).IsRoot a
<VAR>R : Type u<VAR>Semiring R<VAR>x : R<GOAL>Function.Surjective (Polynomial.eval x)
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<GOAL>p.comp q = p.sum fun e a => Polynomial.C a * q ^ e
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>p.comp Polynomial.X = p
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>Polynomial.X.comp p = p
<VAR>R : Type u<VAR>a : R<VAR>Semiring R<VAR>p : R[X]<GOAL>p.comp (Polynomial.C a) = Polynomial.C (Polynomial.eval a p)
<VAR>R : Type u<VAR>a : R<VAR>Semiring R<VAR>p : R[X]<GOAL>(Polynomial.C a).comp p = Polynomial.C a
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ<GOAL>(↑n).comp p = ↑n
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>(OfNat.ofNat n).comp p = ↑n
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>p.comp 0 = Polynomial.C (Polynomial.eval 0 p)
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>Polynomial.comp 0 p = 0
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>p.comp 1 = Polynomial.C (Polynomial.eval 1 p)
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>Polynomial.comp 1 p = 1
<VAR>R : Type u<VAR>Semiring R<VAR>p q r : R[X]<GOAL>(p + q).comp r = p.comp r + q.comp r
<VAR>R : Type u<VAR>a : R<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ<GOAL>((Polynomial.monomial n) a).comp p = Polynomial.C a * p ^ n
<VAR>R : Type u<VAR>Semiring R<VAR>p r : R[X]<GOAL>(p * Polynomial.X).comp r = p.comp r * r
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>k : ℕ<GOAL>(Polynomial.X ^ k).comp p = p ^ k
<VAR>R : Type u<VAR>Semiring R<VAR>p r : R[X]<VAR>k : ℕ<GOAL>(p * Polynomial.X ^ k).comp r = p.comp r * r ^ k
<VAR>R : Type u<VAR>a : R<VAR>Semiring R<VAR>p r : R[X]<GOAL>(Polynomial.C a * p).comp r = Polynomial.C a * p.comp r
<VAR>R : Type u<VAR>Semiring R<VAR>p r : R[X]<VAR>n : ℕ<GOAL>(↑n * p).comp r = ↑n * p.comp r
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<VAR>n : ℕ<GOAL>(p * (Polynomial.X + ↑n)).comp q = p.comp q * (q + ↑n)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>p q r : R[X]<GOAL>(p * q).comp r = p.comp r * q.comp r
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>p q : R[X]<VAR>n : ℕ<GOAL>(p ^ n).comp q = p.comp q ^ n
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Monoid S<VAR>DistribMulAction S R<VAR>IsScalarTower S R R<VAR>s : S<VAR>p q : R[X]<GOAL>(s • p).comp q = s • p.comp q
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>φ ψ χ : R[X]<GOAL>(φ.comp ψ).comp χ = φ.comp (ψ.comp χ)
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<VAR>hqd0 : q.natDegree ≠ 0<GOAL>(p.comp q).coeff (p.natDegree * q.natDegree) = p.leadingCoeff * q.leadingCoeff ^ p.natDegree
<VAR>R : Type u<VAR>ι : Type y<VAR>Semiring R<VAR>s : Finset ι<VAR>p : ι → R[X]<VAR>q : R[X]<GOAL>(∑ i ∈ s, p i).comp q = ∑ i ∈ s, (p i).comp q
<VAR>R : Type u<VAR>S : Type v<VAR>a : R<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<GOAL>Polynomial.map f (Polynomial.C a) = Polynomial.C (f a)
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<GOAL>Polynomial.map f Polynomial.X = Polynomial.X
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>n : ℕ<VAR>a : R<GOAL>Polynomial.map f ((Polynomial.monomial n) a) = (Polynomial.monomial n) (f a)
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<GOAL>Polynomial.map f 0 = 0
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>p q : R[X]<VAR>Semiring S<VAR>f : R →+* S<GOAL>Polynomial.map f (p + q) = Polynomial.map f p + Polynomial.map f q
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<GOAL>Polynomial.map f 1 = 1
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>p q : R[X]<VAR>Semiring S<VAR>f : R →+* S<GOAL>Polynomial.map f (p * q) = Polynomial.map f p * Polynomial.map f q
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>p : R[X]<VAR>Semiring S<VAR>f : R →+* S<VAR>r : R<GOAL>Polynomial.map f (r • p) = f r • Polynomial.map f p
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<GOAL>⇑(Polynomial.mapRingHom f) = Polynomial.map f
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>n : ℕ<GOAL>Polynomial.map f ↑n = ↑n
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>Polynomial.map f (OfNat.ofNat n) = OfNat.ofNat n
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>x y : R[X]<GOAL>x ∣ y → Polynomial.map f x ∣ Polynomial.map f y
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>p : R[X]<VAR>Semiring S<VAR>f : R →+* S<VAR>n : ℕ<GOAL>(Polynomial.map f p).coeff n = f (p.coeff n)
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>e : R ≃+* S<VAR>a : S[X]<GOAL>(Polynomial.mapEquiv e).symm a = Polynomial.map (↑e.symm) a
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>e : R ≃+* S<VAR>a : R[X]<GOAL>(Polynomial.mapEquiv e) a = Polynomial.map (↑e) a
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>Semiring T<VAR>g : S →+* T<VAR>p : R[X]<GOAL>Polynomial.map g (Polynomial.map f p) = Polynomial.map (g.comp f) p
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>Polynomial.map (RingHom.id R) p = p
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>p : R[X]<VAR>Semiring S<VAR>f : R →+* S<VAR>x : S<GOAL>Polynomial.eval₂ f x p = Polynomial.eval x (Polynomial.map f p)
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>hf : Function.Injective ⇑f<GOAL>Function.Injective (Polynomial.map f)
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<GOAL>Function.Surjective (Polynomial.map f)
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>p : R[X]<GOAL>(Polynomial.map f p).degree ≤ p.degree
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>p : R[X]<GOAL>(Polynomial.map f p).natDegree ≤ p.natDegree
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>p : R[X]<VAR>Semiring S<VAR>f : R →+* S<VAR>hf : Function.Injective ⇑f<GOAL>Polynomial.map f p = 0 ↔ p = 0
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>p : R[X]<VAR>Semiring S<VAR>f : R →+* S<VAR>hf : Function.Injective ⇑f<GOAL>Polynomial.map f p ≠ 0 ↔ p ≠ 0
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>p : R[X]<VAR>Semiring S<VAR>f : R →+* S<VAR>hp : p.Monic<GOAL>Polynomial.map f p = 0 ↔ ∀ (x : R), f x = 0
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>p : R[X]<VAR>Semiring S<VAR>f : R →+* S<VAR>hp : p.Monic<VAR>Nontrivial S<GOAL>Polynomial.map f p ≠ 0
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>p : R[X]<VAR>Semiring S<VAR>f : R →+* S<VAR>hf : f p.leadingCoeff ≠ 0<GOAL>(Polynomial.map f p).degree = p.degree
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>p : R[X]<VAR>Semiring S<VAR>f : R →+* S<VAR>hf : f p.leadingCoeff ≠ 0<GOAL>(Polynomial.map f p).natDegree = p.natDegree
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>p : R[X]<VAR>Semiring S<VAR>f : R →+* S<VAR>hf : f p.leadingCoeff ≠ 0<GOAL>(Polynomial.map f p).leadingCoeff = f p.leadingCoeff
<VAR>R : Type u<VAR>Semiring R<GOAL>Polynomial.mapRingHom (RingHom.id R) = RingHom.id R[X]
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>Semiring R<VAR>Semiring S<VAR>Semiring T<VAR>f : S →+* T<VAR>g : R →+* S<GOAL>(Polynomial.mapRingHom f).comp (Polynomial.mapRingHom g) = Polynomial.mapRingHom (f.comp g)
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>L : List R[X]<GOAL>Polynomial.map f L.prod = (List.map (Polynomial.map f) L).prod
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>p : R[X]<VAR>Semiring S<VAR>f : R →+* S<VAR>n : ℕ<GOAL>Polynomial.map f (p ^ n) = Polynomial.map f p ^ n
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>p : S[X]<GOAL>p ∈ (Polynomial.mapRingHom f).rangeS ↔ ∀ (n : ℕ), p.coeff n ∈ f.rangeS
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<VAR>p : S[X]<GOAL>p ∈ (Polynomial.mapRingHom f).range ↔ ∀ (n : ℕ), p.coeff n ∈ f.range
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>Semiring R<VAR>p : R[X]<VAR>Semiring S<VAR>f : R →+* S<VAR>Semiring T<VAR>g : S →+* T<VAR>x : T<GOAL>Polynomial.eval₂ g x (Polynomial.map f p) = Polynomial.eval₂ (g.comp f) x p
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>p : R[X]<VAR>Semiring S<VAR>f : R →+* S<VAR>x : S<GOAL>Polynomial.eval x (Polynomial.map f p) = Polynomial.eval₂ f x p
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>ι : Type u_1<VAR>g : ι → R[X]<VAR>s : Finset ι<GOAL>Polynomial.map f (∑ i ∈ s, g i) = ∑ i ∈ s, Polynomial.map f (g i)
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>p q : R[X]<GOAL>Polynomial.map f (p.comp q) = (Polynomial.map f p).comp (Polynomial.map f q)
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>p : R[X]<GOAL>Polynomial.eval 0 (Polynomial.map f p) = f (Polynomial.eval 0 p)
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>p : R[X]<GOAL>Polynomial.eval 1 (Polynomial.map f p) = f (Polynomial.eval 1 p)
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>p : R[X]<VAR>n : ℕ<GOAL>Polynomial.eval (↑n) (Polynomial.map f p) = f (Polynomial.eval (↑n) p)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<VAR>p : R[X]<VAR>i : ℤ<GOAL>Polynomial.eval (↑i) (Polynomial.map f p) = f (Polynomial.eval (↑i) p)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>Semiring R<VAR>p : R[X]<VAR>Semiring S<VAR>Semiring T<VAR>f : R →+* S<VAR>g : S →+* T<VAR>x : S<GOAL>g (Polynomial.eval₂ f x p) = Polynomial.eval₂ (g.comp f) (g x) p
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>p : R[X]<VAR>Semiring S<VAR>f : R →+* S<VAR>x : R<GOAL>Polynomial.eval₂ f (f x) p = f (Polynomial.eval x p)
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>p q : R[X]<VAR>CommSemiring S<VAR>f : R →+* S<VAR>x : S<GOAL>Polynomial.eval₂ f x (p.comp q) = Polynomial.eval₂ f (Polynomial.eval₂ f x q) p
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>p q : R[X]<VAR>CommSemiring S<VAR>f : R →+* S<VAR>k : ℕ<VAR>t : S<GOAL>Polynomial.eval₂ f t (p.comp^[k] q) = (fun x => Polynomial.eval₂ f x p)^[k] (Polynomial.eval₂ f t q)
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>x : S<VAR>p q : R[X]<GOAL>Polynomial.eval₂ (algebraMap R S) x (p * q) = Polynomial.eval₂ (algebraMap R S) x p * Polynomial.eval₂ (algebraMap R S) x q
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>x : S<VAR>p : R[X]<VAR>n : ℕ<GOAL>Polynomial.eval₂ (algebraMap R S) x (p ^ n) = Polynomial.eval₂ (algebraMap R S) x p ^ n
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>x : S<VAR>p q : R[X]<GOAL>Polynomial.eval₂ (algebraMap R S) x (p.comp q) = Polynomial.eval₂ (algebraMap R S) (Polynomial.eval₂ (algebraMap R S) x q) p
<VAR>R : Type u<VAR>CommSemiring R<VAR>p q : R[X]<VAR>x : R<GOAL>Polynomial.eval x (p * q) = Polynomial.eval x p * Polynomial.eval x q
<VAR>R : Type u<VAR>CommSemiring R<VAR>r : R<GOAL>⇑(Polynomial.evalRingHom r) = Polynomial.eval r
<GOAL>Polynomial.evalRingHom 0 = Polynomial.constantCoeff
<VAR>R : Type u<VAR>CommSemiring R<VAR>p : R[X]<VAR>x : R<VAR>n : ℕ<GOAL>Polynomial.eval x (p ^ n) = Polynomial.eval x p ^ n
<VAR>R : Type u<VAR>CommSemiring R<VAR>p q : R[X]<VAR>x : R<GOAL>Polynomial.eval x (p.comp q) = Polynomial.eval (Polynomial.eval x q) p
<VAR>R : Type u<VAR>CommSemiring R<VAR>p q : R[X]<VAR>k : ℕ<VAR>t : R<GOAL>Polynomial.eval t (p.comp^[k] q) = (fun x => Polynomial.eval x p)^[k] (Polynomial.eval t q)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>p q : R[X]<VAR>r : R<GOAL>(p.comp q).IsRoot r ↔ p.IsRoot (Polynomial.eval r q)
<VAR>R : Type u<VAR>CommSemiring R<VAR>q : R[X]<GOAL>⇑q.compRingHom = fun p => p.comp q
<VAR>R : Type u<VAR>CommSemiring R<VAR>p q : R[X]<GOAL>q.compRingHom p = p.comp q
<VAR>R : Type u<VAR>a : R<VAR>CommSemiring R<VAR>p : R[X]<VAR>q : R[X]<GOAL>q.IsRoot a → (p * q).IsRoot a
<VAR>R : Type u<VAR>a : R<VAR>CommSemiring R<VAR>p : R[X]<VAR>q : R[X]<GOAL>p.IsRoot a → (p * q).IsRoot a
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>CommSemiring S<VAR>f : R →+* S<VAR>s : Multiset R[X]<VAR>x : S<GOAL>Polynomial.eval₂ f x s.prod = (Multiset.map (Polynomial.eval₂ f x) s).prod
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type y<VAR>CommSemiring R<VAR>CommSemiring S<VAR>f : R →+* S<VAR>s : Finset ι<VAR>g : ι → R[X]<VAR>x : S<GOAL>Polynomial.eval₂ f x (∏ i ∈ s, g i) = ∏ i ∈ s, Polynomial.eval₂ f x (g i)
<VAR>R : Type u<VAR>CommSemiring R<VAR>l : List R[X]<VAR>x : R<GOAL>Polynomial.eval x l.prod = (List.map (Polynomial.eval x) l).prod
<VAR>R : Type u<VAR>CommSemiring R<VAR>s : Multiset R[X]<VAR>x : R<GOAL>Polynomial.eval x s.prod = (Multiset.map (Polynomial.eval x) s).prod
<VAR>R : Type u<VAR>CommSemiring R<VAR>ι : Type u_1<VAR>s : Finset ι<VAR>p : ι → R[X]<VAR>x : R<GOAL>Polynomial.eval x (∏ j ∈ s, p j) = ∏ j ∈ s, Polynomial.eval x (p j)
<VAR>R : Type u<VAR>CommSemiring R<VAR>l : List R[X]<VAR>q : R[X]<GOAL>l.prod.comp q = (List.map (fun p => p.comp q) l).prod
<VAR>R : Type u<VAR>CommSemiring R<VAR>s : Multiset R[X]<VAR>q : R[X]<GOAL>s.prod.comp q = (Multiset.map (fun p => p.comp q) s).prod
<VAR>R : Type u<VAR>CommSemiring R<VAR>ι : Type u_1<VAR>s : Finset ι<VAR>p : ι → R[X]<VAR>q : R[X]<GOAL>(∏ j ∈ s, p j).comp q = ∏ j ∈ s, (p j).comp q
<VAR>R : Type u_2<VAR>CommRing R<VAR>IsDomain R<VAR>ι : Type u_1<VAR>s : Finset ι<VAR>p : ι → R[X]<VAR>x : R<GOAL>(∏ j ∈ s, p j).IsRoot x ↔ ∃ i ∈ s, (p i).IsRoot x
<VAR>R : Type u<VAR>CommSemiring R<VAR>p q : R[X]<VAR>x : R<GOAL>p ∣ q → Polynomial.eval x p ∣ Polynomial.eval x q
<VAR>R : Type u<VAR>CommSemiring R<VAR>p q : R[X]<VAR>x : R<GOAL>p ∣ q → Polynomial.eval x p = 0 → Polynomial.eval x q = 0
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>n : ℕ<VAR>x : R<GOAL>Polynomial.eval x (∑ i ∈ Finset.range n, Polynomial.X ^ i) = ∑ i ∈ Finset.range n, x ^ i
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>p : R[X]<GOAL>(Polynomial.map f p).support ⊆ p.support
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>p : R[X]<VAR>f : R →+* S<VAR>hf : Function.Injective ⇑f<GOAL>(Polynomial.map f p).support = p.support
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>CommSemiring S<VAR>f : R →+* S<VAR>m : Multiset R[X]<GOAL>Polynomial.map f m.prod = (Multiset.map (Polynomial.map f) m).prod
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>CommSemiring S<VAR>f : R →+* S<VAR>ι : Type u_1<VAR>g : ι → R[X]<VAR>s : Finset ι<GOAL>Polynomial.map f (∏ i ∈ s, g i) = ∏ i ∈ s, Polynomial.map f (g i)
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>CommSemiring S<VAR>f : R →+* S<VAR>x : R<VAR>p : R[X]<VAR>h : p.IsRoot x<GOAL>(Polynomial.map f p).IsRoot (f x)
<VAR>S : Type v<VAR>CommSemiring S<VAR>R : Type u_1<VAR>CommRing R<VAR>f : R →+* S<VAR>x : R<VAR>p : R[X]<VAR>h : (Polynomial.map f p).IsRoot (f x)<VAR>hf : Function.Injective ⇑f<GOAL>p.IsRoot x
<VAR>S : Type v<VAR>CommSemiring S<VAR>R : Type u_1<VAR>CommRing R<VAR>f : R →+* S<VAR>x : R<VAR>p : R[X]<VAR>hf : Function.Injective ⇑f<GOAL>(Polynomial.map f p).IsRoot (f x) ↔ p.IsRoot x
<VAR>R : Type u<VAR>Ring R<VAR>p q : R[X]<VAR>S : Type u_1<VAR>Ring S<VAR>f : R →+* S<GOAL>Polynomial.map f (p - q) = Polynomial.map f p - Polynomial.map f q
<VAR>R : Type u<VAR>Ring R<VAR>p : R[X]<VAR>S : Type u_1<VAR>Ring S<VAR>f : R →+* S<GOAL>Polynomial.map f (-p) = -Polynomial.map f p
<VAR>R : Type u<VAR>Ring R<VAR>S : Type u_1<VAR>Ring S<VAR>f : R →+* S<VAR>n : ℤ<GOAL>Polynomial.map f ↑n = ↑n
<VAR>R : Type u<VAR>Ring R<VAR>n : ℤ<VAR>x : R<GOAL>Polynomial.eval x ↑n = ↑n
<VAR>R : Type u<VAR>Ring R<VAR>p : R[X]<VAR>S : Type u_1<VAR>Ring S<VAR>f : R →+* S<VAR>x : S<GOAL>Polynomial.eval₂ f x (-p) = -Polynomial.eval₂ f x p
<VAR>R : Type u<VAR>Ring R<VAR>p q : R[X]<VAR>S : Type u_1<VAR>Ring S<VAR>f : R →+* S<VAR>x : S<GOAL>Polynomial.eval₂ f x (p - q) = Polynomial.eval₂ f x p - Polynomial.eval₂ f x q
<VAR>R : Type u<VAR>Ring R<VAR>p : R[X]<VAR>x : R<GOAL>Polynomial.eval x (-p) = -Polynomial.eval x p
<VAR>R : Type u<VAR>Ring R<VAR>p q : R[X]<VAR>x : R<GOAL>Polynomial.eval x (p - q) = Polynomial.eval x p - Polynomial.eval x q
<VAR>R : Type u<VAR>a b : R<VAR>Ring R<GOAL>(Polynomial.X - Polynomial.C a).IsRoot b ↔ a = b
<VAR>R : Type u<VAR>Ring R<VAR>p q : R[X]<GOAL>(-p).comp q = -p.comp q
<VAR>R : Type u<VAR>Ring R<VAR>p q r : R[X]<GOAL>(p - q).comp r = p.comp r - q.comp r
<VAR>R : Type u<VAR>Ring R<VAR>p : R[X]<VAR>i : ℤ<GOAL>(↑i).comp p = ↑i
<VAR>R : Type u<VAR>Ring R<VAR>p : R[X]<VAR>S : Type u_1<VAR>Ring S<VAR>f : R →+* S<VAR>n : ℤ<GOAL>Polynomial.eval₂ f (↑n) p = f (Polynomial.eval (↑n) p)
<VAR>R : Type u<VAR>Ring R<VAR>p q : R[X]<VAR>n : ℕ<GOAL>(p * (Polynomial.X - ↑n)).comp q = p.comp q * (q - ↑n)
<VAR>α : Type u_1<VAR>OrderedCommMonoid α<VAR>s : Set α<VAR>x : α<VAR>hs : IsUpperSet s<VAR>hx : 1 ≤ x<GOAL>x • s ⊆ s
<VAR>α : Type u_1<VAR>OrderedAddCommMonoid α<VAR>s : Set α<VAR>x : α<VAR>hs : IsUpperSet s<VAR>hx : 0 ≤ x<GOAL>x +ᵥ s ⊆ s
<VAR>α : Type u_1<VAR>OrderedCommMonoid α<VAR>s : Set α<VAR>x : α<VAR>hs : IsLowerSet s<VAR>hx : x ≤ 1<GOAL>x • s ⊆ s
<VAR>α : Type u_1<VAR>OrderedAddCommMonoid α<VAR>s : Set α<VAR>x : α<VAR>hs : IsLowerSet s<VAR>hx : x ≤ 0<GOAL>x +ᵥ s ⊆ s
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>s : Set α<VAR>a : α<VAR>hs : IsUpperSet s<GOAL>IsUpperSet (a +ᵥ s)