ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>SMulCommClass R S S<VAR>Pow S ℕ<VAR>NatPowAssoc S<VAR>x : S<VAR>n : ℕ<GOAL>((Polynomial.monomial n) r * p).smeval x = r • (x ^ n * p.smeval x)
<VAR>R : Type u_1<VAR>Semiring R<VAR>p q : Polynomial R<VAR>S : Type u_2<VAR>NonAssocSemiring S<VAR>Module R S<VAR>IsScalarTower R S S<VAR>SMulCommClass R S S<VAR>Pow S ℕ<VAR>NatPowAssoc S<VAR>x : S<GOAL>(p * q).smeval x = p.smeval x * q.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>SMulCommClass R S S<VAR>Pow S ℕ<VAR>NatPowAssoc S<VAR>x : S<VAR>n : ℕ<GOAL>(p ^ n).smeval x = p.smeval x ^ n
<VAR>R : Type u_1<VAR>Semiring R<VAR>p q : Polynomial R<VAR>S : Type u_2<VAR>NonAssocSemiring S<VAR>Module R S<VAR>IsScalarTower R S S<VAR>SMulCommClass R S S<VAR>Pow S ℕ<VAR>NatPowAssoc S<VAR>x : S<GOAL>(p.comp q).smeval x = p.smeval (q.smeval x)
<VAR>R : Type u_1<VAR>Semiring R<VAR>p : Polynomial R<VAR>S : Type u_2<VAR>Semiring S<VAR>Module R S<VAR>IsScalarTower R S S<VAR>SMulCommClass R S S<VAR>x y : S<VAR>hc : Commute x y<GOAL>Commute (p.smeval x) y
<VAR>R : Type u_1<VAR>Semiring R<VAR>p q : Polynomial R<VAR>S : Type u_2<VAR>Semiring S<VAR>Module R S<VAR>IsScalarTower R S S<VAR>SMulCommClass R S S<VAR>x y : S<VAR>hc : Commute x y<GOAL>Commute (p.smeval x) (q.smeval y)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Type u_2<VAR>Semiring S<VAR>Algebra R S<VAR>x : S<VAR>p : Polynomial R<GOAL>(Polynomial.aeval x) p = p.smeval x
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Type u_2<VAR>Semiring S<VAR>Algebra R S<VAR>x : S<GOAL>⇑(Polynomial.aeval x) = fun p => p.smeval x
<VAR>R : Type u<VAR>Semiring R<VAR>M : Polynomial R → Prop<VAR>p : Polynomial R<VAR>h_C : ∀ (a : R), M (Polynomial.C a)<VAR>h_add : ∀ (p q : Polynomial R), M p → M q → M (p + q)<VAR>h_monomial : ∀ (n : ℕ) (a : R), M (Polynomial.C a * Polynomial.X ^ n) → M (Polynomial.C a * Polynomial.X ^ (n + 1))<GOAL>M p
<VAR>R : Type u<VAR>Semiring R<VAR>M : Polynomial R → Prop<VAR>p : Polynomial R<VAR>h_add : ∀ (p q : Polynomial R), M p → M q → M (p + q)<VAR>h_monomial : ∀ (n : ℕ) (a : R), M ((Polynomial.monomial n) a)<GOAL>M p
<VAR>R : Type u<VAR>Semiring R<VAR>f : Polynomial R<VAR>I : Ideal (Polynomial R)<VAR>cf : ∀ (i : ℕ), Polynomial.C (f.coeff i) ∈ I<GOAL>Ideal.span {g | ∃ i, g = Polynomial.C (f.coeff i)} ≤ I
<VAR>R : Type u<VAR>Semiring R<VAR>f : Polynomial R<GOAL>f ∈ Ideal.span {g | ∃ i, g = Polynomial.C (f.coeff i)}
<VAR>R : Type u<VAR>Semiring R<VAR>f : Polynomial R<VAR>I : Ideal (Polynomial R)<GOAL>f ∉ I → ∃ i, Polynomial.C (f.coeff i) ∉ I
<VAR>K : Type v<VAR>L : Type w<VAR>CommRing K<VAR>Field L<VAR>i : K →+* L<GOAL>Polynomial.Splits i 0
<VAR>K : Type v<VAR>L : Type w<VAR>CommRing K<VAR>Field L<VAR>i : K →+* L<VAR>f : K[X]<VAR>a : L<VAR>h : Polynomial.map i f = Polynomial.C a<GOAL>Polynomial.Splits i f
<VAR>K : Type v<VAR>L : Type w<VAR>CommRing K<VAR>Field L<VAR>i : K →+* L<VAR>a : K<GOAL>Polynomial.Splits i (Polynomial.C a)
<VAR>K : Type v<VAR>L : Type w<VAR>CommRing K<VAR>Field L<VAR>i : K →+* L<VAR>f : K[X]<VAR>hf : (Polynomial.map i f).degree = 1<GOAL>Polynomial.Splits i f
<VAR>K : Type v<VAR>L : Type w<VAR>CommRing K<VAR>Field L<VAR>i : K →+* L<VAR>f : K[X]<VAR>hf : f.degree ≤ 1<GOAL>Polynomial.Splits i f
<VAR>K : Type v<VAR>L : Type w<VAR>CommRing K<VAR>Field L<VAR>i : K →+* L<VAR>f : K[X]<VAR>hf : f.degree = 1<GOAL>Polynomial.Splits i f
<VAR>K : Type v<VAR>L : Type w<VAR>CommRing K<VAR>Field L<VAR>i : K →+* L<VAR>f : K[X]<VAR>hf : f.natDegree ≤ 1<GOAL>Polynomial.Splits i f
<VAR>K : Type v<VAR>L : Type w<VAR>CommRing K<VAR>Field L<VAR>i : K →+* L<VAR>f : K[X]<VAR>hf : f.natDegree = 1<GOAL>Polynomial.Splits i f
<VAR>K : Type v<VAR>L : Type w<VAR>CommRing K<VAR>Field L<VAR>i : K →+* L<VAR>f g : K[X]<VAR>hf : Polynomial.Splits i f<VAR>hg : Polynomial.Splits i g<GOAL>Polynomial.Splits i (f * g)
<VAR>K : Type v<VAR>L : Type w<VAR>CommRing K<VAR>Field L<VAR>i : K →+* L<VAR>f g : K[X]<VAR>hfg : Polynomial.map i (f * g) ≠ 0<VAR>h : Polynomial.Splits i (f * g)<GOAL>Polynomial.Splits i f ∧ Polynomial.Splits i g
<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>CommRing K<VAR>Field L<VAR>Field F<VAR>i : K →+* L<VAR>j : L →+* F<VAR>f : K[X]<GOAL>Polynomial.Splits j (Polynomial.map i f) ↔ Polynomial.Splits (j.comp i) f
<VAR>K : Type v<VAR>L : Type w<VAR>CommRing K<VAR>Field L<VAR>i : K →+* L<GOAL>Polynomial.Splits i 1
<VAR>K : Type v<VAR>L : Type w<VAR>CommRing K<VAR>Field L<VAR>i : K →+* L<VAR>IsDomain K<VAR>u : K[X]<VAR>hu : IsUnit u<GOAL>Polynomial.Splits i u
<VAR>K : Type v<VAR>L : Type w<VAR>CommRing K<VAR>Field L<VAR>i : K →+* L<VAR>x : K<GOAL>Polynomial.Splits i (Polynomial.X - Polynomial.C x)
<VAR>K : Type v<VAR>L : Type w<VAR>CommRing K<VAR>Field L<VAR>i : K →+* L<GOAL>Polynomial.Splits i Polynomial.X
<VAR>K : Type v<VAR>L : Type w<VAR>CommRing K<VAR>Field L<VAR>i : K →+* L<VAR>ι : Type u<VAR>s : ι → K[X]<VAR>t : Finset ι<GOAL>(∀ j ∈ t, Polynomial.Splits i (s j)) → Polynomial.Splits i (∏ x ∈ t, s x)
<VAR>K : Type v<VAR>L : Type w<VAR>CommRing K<VAR>Field L<VAR>i : K →+* L<VAR>f : K[X]<VAR>hf : Polynomial.Splits i f<VAR>n : ℕ<GOAL>Polynomial.Splits i (f ^ n)
<VAR>K : Type v<VAR>L : Type w<VAR>CommRing K<VAR>Field L<VAR>i : K →+* L<VAR>n : ℕ<GOAL>Polynomial.Splits i (Polynomial.X ^ n)
<VAR>K : Type v<VAR>L : Type w<VAR>CommRing K<VAR>Field L<VAR>i : K →+* L<VAR>f : K[X]<GOAL>Polynomial.Splits (RingHom.id L) (Polynomial.map i f) ↔ Polynomial.Splits i f
<VAR>K : Type v<VAR>L : Type w<VAR>CommRing K<VAR>Field L<VAR>i : K →+* L<VAR>f : K[X]<VAR>hs : Polynomial.Splits i f<VAR>hf0 : (Polynomial.map i f).degree ≠ 0<GOAL>∃ x, Polynomial.eval₂ i x f = 0
<VAR>K : Type v<VAR>L : Type w<VAR>CommRing K<VAR>Field L<VAR>i : K →+* L<VAR>f : K[X]<VAR>hs : Polynomial.Splits i f<VAR>hf0 : (Polynomial.map i f).natDegree ≠ 0<GOAL>(Polynomial.map i f).roots ≠ 0
<VAR>K : Type v<VAR>L : Type w<VAR>CommRing K<VAR>Field L<VAR>i : K →+* L<VAR>f : K[X]<VAR>hf : Polynomial.Splits i f<VAR>hfd : (Polynomial.map i f).degree ≠ 0<GOAL>Polynomial.eval₂ i (Polynomial.rootOfSplits' i hf hfd) f = 0
<VAR>K : Type v<VAR>L : Type w<VAR>CommRing K<VAR>Field L<VAR>p : K[X]<VAR>i : K →+* L<VAR>hsplit : Polynomial.Splits i p<GOAL>(Polynomial.map i p).natDegree = Multiset.card (Polynomial.map i p).roots
<VAR>K : Type v<VAR>L : Type w<VAR>CommRing K<VAR>Field L<VAR>p : K[X]<VAR>i : K →+* L<VAR>p_ne_zero : Polynomial.map i p ≠ 0<VAR>hsplit : Polynomial.Splits i p<GOAL>(Polynomial.map i p).degree = ↑(Multiset.card (Polynomial.map i p).roots)
<VAR>K : Type v<VAR>L : Type w<VAR>Field K<VAR>Field L<VAR>i : K →+* L<VAR>f : K[X]<GOAL>Polynomial.Splits i f ↔ f = 0 ∨ ∀ {g : L[X]}, Irreducible g → g ∣ Polynomial.map i f → g.degree = 1
<VAR>K : Type v<VAR>L : Type w<VAR>Field K<VAR>Field L<VAR>i : K →+* L<VAR>f : K[X]<VAR>h : Polynomial.Splits i f<GOAL>f = 0 ∨ ∀ {g : L[X]}, Irreducible g → g ∣ Polynomial.map i f → g.degree = 1
<VAR>K : Type v<VAR>L : Type w<VAR>Field K<VAR>Field L<VAR>i : K →+* L<VAR>f g : K[X]<VAR>hfg : f * g ≠ 0<VAR>h : Polynomial.Splits i (f * g)<GOAL>Polynomial.Splits i f ∧ Polynomial.Splits i g
<VAR>K : Type v<VAR>L : Type w<VAR>Field K<VAR>Field L<VAR>i : K →+* L<VAR>f g : K[X]<VAR>hf0 : f ≠ 0<VAR>hf : Polynomial.Splits i f<VAR>hgf : g ∣ f<GOAL>Polynomial.Splits i g
<VAR>K : Type v<VAR>L : Type w<VAR>Field K<VAR>Field L<VAR>i : K →+* L<VAR>DecidableEq K<VAR>f g : K[X]<VAR>hf0 : f ≠ 0<VAR>hf : Polynomial.Splits i f<GOAL>Polynomial.Splits i (EuclideanDomain.gcd f g)
<VAR>K : Type v<VAR>L : Type w<VAR>Field K<VAR>Field L<VAR>i : K →+* L<VAR>DecidableEq K<VAR>f g : K[X]<VAR>hg0 : g ≠ 0<VAR>hg : Polynomial.Splits i g<GOAL>Polynomial.Splits i (EuclideanDomain.gcd f g)
<VAR>K : Type v<VAR>L : Type w<VAR>Field K<VAR>Field L<VAR>i : K →+* L<VAR>f g : K[X]<VAR>hf : f ≠ 0<VAR>hg : g ≠ 0<GOAL>Polynomial.Splits i (f * g) ↔ Polynomial.Splits i f ∧ Polynomial.Splits i g
<VAR>K : Type v<VAR>L : Type w<VAR>Field K<VAR>Field L<VAR>i : K →+* L<VAR>ι : Type u<VAR>s : ι → K[X]<VAR>t : Finset ι<GOAL>(∀ j ∈ t, s j ≠ 0) → (Polynomial.Splits i (∏ x ∈ t, s x) ↔ ∀ j ∈ t, Polynomial.Splits i (s j))
<VAR>K : Type v<VAR>Field K<VAR>p : K[X]<VAR>hp : Irreducible p<VAR>hp_splits : Polynomial.Splits (RingHom.id K) p<GOAL>p.degree = 1
<VAR>K : Type v<VAR>L : Type w<VAR>Field K<VAR>Field L<VAR>i : K →+* L<VAR>f : K[X]<VAR>hs : Polynomial.Splits i f<VAR>hf0 : f.degree ≠ 0<GOAL>∃ x, Polynomial.eval₂ i x f = 0
<VAR>K : Type v<VAR>L : Type w<VAR>Field K<VAR>Field L<VAR>i : K →+* L<VAR>f : K[X]<VAR>hs : Polynomial.Splits i f<VAR>hf0 : f.natDegree ≠ 0<GOAL>(Polynomial.map i f).roots ≠ 0
<VAR>K : Type v<VAR>L : Type w<VAR>Field K<VAR>Field L<VAR>i : K →+* L<VAR>f : K[X]<VAR>hf : Polynomial.Splits i f<VAR>hfd : (Polynomial.map i f).degree ≠ 0<GOAL>Polynomial.rootOfSplits' i hf hfd = Polynomial.rootOfSplits i hf ⋯
<VAR>K : Type v<VAR>L : Type w<VAR>Field K<VAR>Field L<VAR>i : K →+* L<VAR>f : K[X]<VAR>hf : Polynomial.Splits i f<VAR>hfd : f.degree ≠ 0<GOAL>Polynomial.eval₂ i (Polynomial.rootOfSplits i hf hfd) f = 0
<VAR>K : Type v<VAR>L : Type w<VAR>Field K<VAR>Field L<VAR>p : K[X]<VAR>i : K →+* L<VAR>hsplit : Polynomial.Splits i p<GOAL>p.natDegree = Multiset.card (Polynomial.map i p).roots
<VAR>K : Type v<VAR>L : Type w<VAR>Field K<VAR>Field L<VAR>p : K[X]<VAR>i : K →+* L<VAR>p_ne_zero : p ≠ 0<VAR>hsplit : Polynomial.Splits i p<GOAL>p.degree = ↑(Multiset.card (Polynomial.map i p).roots)
<VAR>K : Type v<VAR>L : Type w<VAR>Field K<VAR>Field L<VAR>i : K →+* L<VAR>f : K[X]<VAR>hf : Polynomial.Splits (RingHom.id K) f<GOAL>(Polynomial.map i f).roots = Multiset.map (⇑i) f.roots
<VAR>R : Type u_1<VAR>K : Type v<VAR>L : Type w<VAR>CommRing R<VAR>Field K<VAR>Field L<VAR>Algebra R K<VAR>Algebra R L<VAR>p : R[X]<VAR>h : Polynomial.Splits (algebraMap R K) p<VAR>f : K →ₐ[R] L<GOAL>⇑f '' p.rootSet K = p.rootSet L
<VAR>R : Type u_1<VAR>K : Type v<VAR>L : Type w<VAR>CommRing R<VAR>Field K<VAR>Field L<VAR>Algebra R K<VAR>Algebra R L<VAR>p : R[X]<VAR>h : Polynomial.Splits (algebraMap R K) p<VAR>f : K →ₐ[R] L<GOAL>Algebra.adjoin R (p.rootSet L) = f.range ↔ Algebra.adjoin R (p.rootSet K) = ⊤
<VAR>K : Type v<VAR>L : Type w<VAR>Field K<VAR>Field L<VAR>p : K[X]<VAR>i : K →+* L<VAR>hsplit : Polynomial.Splits i p<GOAL>Polynomial.map i p = Polynomial.C (i p.leadingCoeff) * (Multiset.map (fun a => Polynomial.X - Polynomial.C a) (Polynomial.map i p).roots).prod
<VAR>K : Type v<VAR>Field K<VAR>p : K[X]<VAR>hsplit : Polynomial.Splits (RingHom.id K) p<GOAL>p = Polynomial.C p.leadingCoeff * (Multiset.map (fun a => Polynomial.X - Polynomial.C a) p.roots).prod
<VAR>K : Type v<VAR>Field K<VAR>p : K[X]<VAR>m : p.Monic<VAR>hsplit : Polynomial.Splits (RingHom.id K) p<GOAL>p = (Multiset.map (fun a => Polynomial.X - Polynomial.C a) p.roots).prod
<VAR>K : Type v<VAR>L : Type w<VAR>Field K<VAR>Field L<VAR>i : K →+* L<VAR>x : K<VAR>h : K[X]<VAR>h_splits : Polynomial.Splits i h<VAR>h_roots : (Polynomial.map i h).roots = {i x}<GOAL>h = Polynomial.C h.leadingCoeff * (Polynomial.X - Polynomial.C x)
<VAR>R : Type u_1<VAR>K : Type v<VAR>CommRing R<VAR>Field K<VAR>Algebra R K<VAR>f : K[X]<VAR>hs : Polynomial.Splits (RingHom.id K) f<VAR>hm : f.Monic<VAR>hr : ∀ a ∈ f.roots, a ∈ (algebraMap R K).range<GOAL>f ∈ Polynomial.lifts (algebraMap R K)
<VAR>K : Type v<VAR>L : Type w<VAR>Field K<VAR>Field L<VAR>i : K →+* L<VAR>f : K[X]<VAR>s : Multiset L<VAR>hs : Polynomial.map i f = Polynomial.C (i f.leadingCoeff) * (Multiset.map (fun a => Polynomial.X - Polynomial.C a) s).prod<GOAL>Polynomial.Splits i f
<VAR>K : Type v<VAR>L : Type w<VAR>Field K<VAR>Field L<VAR>i : K →+* L<VAR>f : K[X]<GOAL>Polynomial.Splits (RingHom.id K) f → Polynomial.Splits i f
<VAR>K : Type v<VAR>L : Type w<VAR>Field K<VAR>Field L<VAR>i : K →+* L<VAR>f : K[X]<GOAL>Polynomial.Splits i f ↔ ∃ s, Polynomial.map i f = Polynomial.C (i f.leadingCoeff) * (Multiset.map (fun a => Polynomial.X - Polynomial.C a) s).prod
<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>Field K<VAR>Field L<VAR>Field F<VAR>i : K →+* L<VAR>j : L →+* F<VAR>f : K[X]<VAR>h : Polynomial.Splits (j.comp i) f<VAR>roots_mem_range : ∀ a ∈ (Polynomial.map (j.comp i) f).roots, a ∈ j.range<GOAL>Polynomial.Splits i f
<VAR>K : Type v<VAR>L : Type w<VAR>Field K<VAR>Field L<VAR>i : K →+* L<VAR>f : K[X]<VAR>h : Polynomial.Splits i f<VAR>roots_mem_range : ∀ a ∈ (Polynomial.map i f).roots, a ∈ i.range<GOAL>Polynomial.Splits (RingHom.id K) f
<VAR>R : Type u_1<VAR>K : Type v<VAR>L : Type w<VAR>CommRing R<VAR>Field K<VAR>Field L<VAR>i : R →+* K<VAR>j : K →+* L<VAR>f : R[X]<VAR>h : Polynomial.Splits i f<GOAL>Polynomial.Splits (j.comp i) f
<VAR>R : Type u_1<VAR>K : Type v<VAR>L : Type w<VAR>CommRing R<VAR>Field K<VAR>Field L<VAR>Algebra R K<VAR>Algebra R L<VAR>f : R[X]<VAR>h : Polynomial.Splits (algebraMap R K) f<VAR>e : K →ₐ[R] L<GOAL>Polynomial.Splits (algebraMap R L) f
<VAR>R : Type u_1<VAR>K : Type v<VAR>L : Type w<VAR>CommRing R<VAR>Field K<VAR>Field L<VAR>Algebra R K<VAR>Algebra R L<VAR>f : R[X]<VAR>Algebra K L<VAR>IsScalarTower R K L<VAR>h : Polynomial.Splits (algebraMap R K) f<GOAL>Polynomial.Splits (algebraMap R L) f
<VAR>K : Type v<VAR>Field K<VAR>p : K[X]<GOAL>Polynomial.Splits (RingHom.id K) p ↔ Multiset.card p.roots = p.natDegree
<VAR>K : Type v<VAR>L : Type w<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>DecidableEq L<VAR>P : K[X]<VAR>hmo : P.Monic<VAR>hP : Polynomial.Splits (algebraMap K L) P<VAR>r : L<VAR>hr : r ∈ P.aroots L<GOAL>(Polynomial.aeval r) (Polynomial.derivative P) = (Multiset.map (fun a => r - a) ((P.aroots L).erase r)).prod
<VAR>K : Type v<VAR>Field K<VAR>P : K[X]<VAR>hmo : P.Monic<VAR>hP : Polynomial.Splits (RingHom.id K) P<GOAL>P.coeff 0 = (-1) ^ P.natDegree * P.roots.prod
<VAR>K : Type v<VAR>Field K<VAR>P : K[X]<VAR>hmo : P.Monic<VAR>hP : Polynomial.Splits (RingHom.id K) P<GOAL>P.nextCoeff = -P.roots.sum
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>M : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>a : A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module A M<VAR>Module R M<VAR>IsScalarTower R A M<VAR>f : R[X]<VAR>m : M<GOAL>(Module.AEval.of R M a) ((Polynomial.aeval a) f • m) = f • (Module.AEval.of R M a) m
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>M : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>a : A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module A M<VAR>Module R M<VAR>IsScalarTower R A M<VAR>f : R[X]<VAR>m : Module.AEval R M a<GOAL>(Module.AEval.of R M a).symm (f • m) = (Polynomial.aeval a) f • (Module.AEval.of R M a).symm m
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>M : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>a : A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module A M<VAR>Module R M<VAR>IsScalarTower R A M<VAR>t : R<VAR>m : Module.AEval R M a<GOAL>Polynomial.C t • m = t • m
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>M : Type u_1<VAR>CommSemiring R<VAR>Semiring A<VAR>a : A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module A M<VAR>Module R M<VAR>IsScalarTower R A M<VAR>m : M<GOAL>Polynomial.X • (Module.AEval.of R M a) m = (Module.AEval.of R M a) (a • m)
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>M : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>a : A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module A M<VAR>Module R M<VAR>IsScalarTower R A M<VAR>m : Module.AEval R M a<GOAL>(Module.AEval.of R M a).symm (Polynomial.X • m) = a • (Module.AEval.of R M a).symm m
<VAR>R : Type u_3<VAR>A : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>a : A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module A M<VAR>Module R M<VAR>IsScalarTower R A M<VAR>FaithfulSMul A M<GOAL>Module.annihilator R[X] (Module.AEval R M a) = RingHom.ker (Polynomial.aeval a)
<VAR>R : Type u_3<VAR>A : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>a : A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module A M<VAR>Module R M<VAR>IsScalarTower R A M<VAR>FaithfulSMul A M<GOAL>⊤.annihilator = RingHom.ker (Polynomial.aeval a)
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>M : Type u_1<VAR>CommSemiring R<VAR>Semiring A<VAR>a : A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module A M<VAR>Module R M<VAR>IsScalarTower R A M<VAR>q : Submodule R[X] (Module.AEval R M a)<VAR>x : M<GOAL>x ∈ (Module.AEval.comapSubmodule R M a) q ↔ (Module.AEval.of R M a) x ∈ q
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>M : Type u_1<VAR>CommSemiring R<VAR>Semiring A<VAR>a : A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module A M<VAR>Module R M<VAR>IsScalarTower R A M<VAR>q : Submodule R[X] (Module.AEval R M a)<GOAL>(Module.AEval.comapSubmodule R M a) q ≤ Submodule.comap ((Algebra.lsmul R R M) a) ((Module.AEval.comapSubmodule R M a) q)
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>M : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>a : A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module A M<VAR>Module R M<VAR>IsScalarTower R A M<VAR>p : Submodule R M<VAR>hp : p ≤ Submodule.comap ((Algebra.lsmul R R M) a) p<VAR>m : Module.AEval R M a<GOAL>m ∈ Module.AEval.mapSubmodule a hp ↔ (Module.AEval.of R M a).symm m ∈ p
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>M : Type u_1<VAR>CommSemiring R<VAR>Semiring A<VAR>a : A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module A M<VAR>Module R M<VAR>IsScalarTower R A M<VAR>q : Submodule R[X] (Module.AEval R M a)<VAR>h : (Module.AEval.comapSubmodule R M a) q ≤ Submodule.comap ((Algebra.lsmul R R M) a) ((Module.AEval.comapSubmodule R M a) q) := ⋯<GOAL>Module.AEval.mapSubmodule a h = q
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>M : Type u_1<VAR>CommSemiring R<VAR>Semiring A<VAR>a : A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module A M<VAR>Module R M<VAR>IsScalarTower R A M<VAR>p : Submodule R M<VAR>hp : p ≤ Submodule.comap ((Algebra.lsmul R R M) a) p<GOAL>(Module.AEval.comapSubmodule R M a) (Module.AEval.mapSubmodule a hp) = p
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>M : Type u_1<VAR>CommSemiring R<VAR>Semiring A<VAR>a : A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module A M<VAR>Module R M<VAR>IsScalarTower R A M<GOAL>Function.Injective ⇑(Module.AEval.comapSubmodule R M a)
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>M : Type u_1<VAR>CommSemiring R<VAR>Semiring A<VAR>a : A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module A M<VAR>Module R M<VAR>IsScalarTower R A M<GOAL>Set.range ⇑(Module.AEval.comapSubmodule R M a) = {p | p ≤ Submodule.comap ((Algebra.lsmul R R M) a) p}
<VAR>R : Type u_2<VAR>M : Type u_1<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>φ : M →ₗ[R] M<GOAL>Module.AEval' φ = Module.AEval R M φ
<VAR>R : Type u_2<VAR>M : Type u_1<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>φ : M →ₗ[R] M<VAR>m : M<GOAL>Polynomial.X • (Module.AEval'.of φ) m = (Module.AEval'.of φ) (φ m)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>φ : M →ₗ[R] M<VAR>m : Module.AEval' φ<GOAL>(Module.AEval'.of φ).symm (Polynomial.X • m) = φ ((Module.AEval'.of φ).symm m)
<VAR>R : Type u_1<VAR>Ring R<VAR>p q : Polynomial R<GOAL>-p.cancelLeads q = q.cancelLeads p
<VAR>R : Type u_1<VAR>Ring R<VAR>p q : Polynomial R<VAR>comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff<VAR>h : p.natDegree ≤ q.natDegree<VAR>hq : 0 < q.natDegree<GOAL>(p.cancelLeads q).natDegree < q.natDegree
<VAR>R : Type u_1<VAR>CommRing R<VAR>p q r : Polynomial R<VAR>pq : p ∣ q<VAR>pr : p ∣ r<GOAL>p ∣ q.cancelLeads r
<VAR>R : Type u_1<VAR>CommRing R<VAR>p q : Polynomial R<VAR>h : p.natDegree ≤ q.natDegree<VAR>hq : 0 < q.natDegree<GOAL>(p.cancelLeads q).natDegree < q.natDegree
<VAR>R : Type u<VAR>Semiring R<VAR>P : R[X] → Prop<GOAL>(∀ (p : R[X]), P p) ↔ ∀ (q : R[ℕ]), P { toFinsupp := q }
<VAR>R : Type u<VAR>Semiring R<VAR>P : R[X] → Prop<GOAL>(∃ p, P p) ↔ ∃ q, P { toFinsupp := q }
<VAR>R : Type u<VAR>Semiring R<VAR>f : R[X]<GOAL>{ toFinsupp := f.toFinsupp } = f
<VAR>R : Type u_1<VAR>Semiring R<GOAL>∀ (x x_1 : R[X]), Polynomial.add x x_1 = match x, x_1 with | { toFinsupp := a }, { toFinsupp := b } => { toFinsupp := a + b }
<VAR>R : Type u_1<VAR>Ring R<GOAL>∀ (x : R[X]), Polynomial.neg x = match x with | { toFinsupp := a } => { toFinsupp := -a }
<VAR>R : Type u_1<VAR>Semiring R<GOAL>∀ (x x_1 : R[X]), Polynomial.mul x x_1 = match x, x_1 with | { toFinsupp := a }, { toFinsupp := b } => { toFinsupp := a * b }
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<GOAL>Polynomial.add p q = p + q
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<GOAL>Polynomial.mul p q = p * q
<VAR>R : Type u<VAR>Semiring R<GOAL>{ toFinsupp := 0 } = 0
<VAR>R : Type u<VAR>Semiring R<GOAL>{ toFinsupp := 1 } = 1
<VAR>R : Type u<VAR>Semiring R<VAR>a b : R[ℕ]<GOAL>{ toFinsupp := a + b } = { toFinsupp := a } + { toFinsupp := b }
<VAR>R : Type u<VAR>Ring R<VAR>a : R[ℕ]<GOAL>{ toFinsupp := -a } = -{ toFinsupp := a }
<VAR>R : Type u<VAR>Ring R<VAR>a b : R[ℕ]<GOAL>{ toFinsupp := a - b } = { toFinsupp := a } - { toFinsupp := b }
<VAR>R : Type u<VAR>Semiring R<VAR>a b : R[ℕ]<GOAL>{ toFinsupp := a * b } = { toFinsupp := a } * { toFinsupp := b }
<VAR>R : Type u<VAR>Semiring R<VAR>S : Type u_1<VAR>SMulZeroClass S R<VAR>a : S<VAR>b : R[ℕ]<GOAL>{ toFinsupp := a • b } = a • { toFinsupp := b }
<VAR>R : Type u<VAR>Semiring R<VAR>a : R[ℕ]<VAR>n : ℕ<GOAL>{ toFinsupp := a ^ n } = { toFinsupp := a } ^ n
<VAR>R : Type u<VAR>Semiring R<GOAL>Polynomial.toFinsupp 0 = 0
<VAR>R : Type u<VAR>Semiring R<GOAL>Polynomial.toFinsupp 1 = 1
<VAR>R : Type u<VAR>Semiring R<VAR>a b : R[X]<GOAL>(a + b).toFinsupp = a.toFinsupp + b.toFinsupp
<VAR>R : Type u<VAR>Ring R<VAR>a : R[X]<GOAL>(-a).toFinsupp = -a.toFinsupp
<VAR>R : Type u<VAR>Ring R<VAR>a b : R[X]<GOAL>(a - b).toFinsupp = a.toFinsupp - b.toFinsupp
<VAR>R : Type u<VAR>Semiring R<VAR>a b : R[X]<GOAL>(a * b).toFinsupp = a.toFinsupp * b.toFinsupp
<VAR>R : Type u<VAR>Semiring R<VAR>S : Type u_1<VAR>SMulZeroClass S R<VAR>a : S<VAR>b : R[X]<GOAL>(a • b).toFinsupp = a • b.toFinsupp
<VAR>R : Type u<VAR>Semiring R<VAR>a : R[X]<VAR>n : ℕ<GOAL>(a ^ n).toFinsupp = a.toFinsupp ^ n
<VAR>R : Type u<VAR>Semiring R<VAR>S : Type u_1<VAR>Monoid S<VAR>DistribMulAction S R<VAR>a : S<VAR>ha : IsSMulRegular R a<GOAL>IsSMulRegular R[X] a
<VAR>R : Type u<VAR>Semiring R<GOAL>Function.Injective Polynomial.toFinsupp
<VAR>R : Type u<VAR>Semiring R<VAR>a b : R[X]<GOAL>a.toFinsupp = b.toFinsupp ↔ a = b
<VAR>R : Type u<VAR>Semiring R<VAR>a : R[X]<GOAL>a.toFinsupp = 0 ↔ a = 0
<VAR>R : Type u<VAR>Semiring R<VAR>a : R[X]<GOAL>a.toFinsupp = 1 ↔ a = 1
<VAR>R : Type u<VAR>Semiring R<VAR>a b : R[ℕ]<GOAL>{ toFinsupp := a } = { toFinsupp := b } ↔ a = b
<VAR>R : Type u<VAR>Semiring R<VAR>a : R[ℕ]<GOAL>{ toFinsupp := a } = 0 ↔ a = 0
<VAR>R : Type u<VAR>Semiring R<VAR>a : R[ℕ]<GOAL>{ toFinsupp := a } = 1 ↔ a = 1
<VAR>R : Type u<VAR>Semiring R<VAR>toFinsupp : R[ℕ]<GOAL>(Polynomial.toFinsuppIso R).symm toFinsupp = { toFinsupp := toFinsupp }
<VAR>R : Type u<VAR>Semiring R<VAR>self : R[X]<GOAL>(Polynomial.toFinsuppIso R) self = self.toFinsupp
<VAR>R : Type u<VAR>Semiring R<VAR>ι : Type u_1<VAR>s : Finset ι<VAR>f : ι → R[ℕ]<GOAL>{ toFinsupp := ∑ i ∈ s, f i } = ∑ i ∈ s, { toFinsupp := f i }
<VAR>R : Type u<VAR>Semiring R<VAR>ι : Type u_1<VAR>s : Finset ι<VAR>f : ι → R[X]<GOAL>(∑ i ∈ s, f i).toFinsupp = ∑ i ∈ s, (f i).toFinsupp
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[ℕ]<GOAL>{ toFinsupp := p }.support = p.support
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>p.toFinsupp.support = p.support
<VAR>R : Type u<VAR>Semiring R<GOAL>Polynomial.support 0 = ∅
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>p.support = ∅ ↔ p = 0
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>p.support.Nonempty ↔ p ≠ 0
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>p.support.card = 0 ↔ p = 0
<VAR>R : Type u<VAR>Semiring R<VAR>n : ℕ<VAR>r : R<GOAL>((Polynomial.monomial n) r).toFinsupp = Finsupp.single n r
<VAR>R : Type u<VAR>Semiring R<VAR>n : ℕ<VAR>r : R<GOAL>{ toFinsupp := Finsupp.single n r } = (Polynomial.monomial n) r
<VAR>R : Type u<VAR>Semiring R<VAR>n : ℕ<GOAL>(Polynomial.monomial n) 0 = 0
<VAR>R : Type u<VAR>Semiring R<GOAL>(Polynomial.monomial 0) 1 = 1
<VAR>R : Type u<VAR>Semiring R<VAR>n : ℕ<VAR>r s : R<GOAL>(Polynomial.monomial n) (r + s) = (Polynomial.monomial n) r + (Polynomial.monomial n) s
<VAR>R : Type u<VAR>Semiring R<VAR>n m : ℕ<VAR>r s : R<GOAL>(Polynomial.monomial n) r * (Polynomial.monomial m) s = (Polynomial.monomial (n + m)) (r * s)
<VAR>R : Type u<VAR>Semiring R<VAR>n : ℕ<VAR>r : R<VAR>k : ℕ<GOAL>(Polynomial.monomial n) r ^ k = (Polynomial.monomial (n * k)) (r ^ k)