ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>Semiring R<VAR>Nontrivial R<GOAL>Polynomial.trailingDegree 1 = 0
<VAR>R : Type u<VAR>Semiring R<VAR>Nontrivial R<GOAL>Polynomial.X.trailingDegree = 1
<VAR>R : Type u<VAR>Semiring R<VAR>Nontrivial R<GOAL>Polynomial.X.natTrailingDegree = 1
<VAR>R : Type u<VAR>Semiring R<VAR>Nontrivial R<VAR>n : ℕ<GOAL>(Polynomial.X ^ n).trailingDegree = ↑n
<VAR>R : Type u<VAR>Semiring R<VAR>Nontrivial R<VAR>n : ℕ<GOAL>(Polynomial.X ^ n).natTrailingDegree = n
<VAR>R : Type u<VAR>Ring R<VAR>p : R[X]<GOAL>(-p).trailingDegree = p.trailingDegree
<VAR>R : Type u<VAR>Ring R<VAR>p : R[X]<GOAL>(-p).natTrailingDegree = p.natTrailingDegree
<VAR>R : Type u<VAR>Ring R<VAR>n : ℤ<GOAL>(↑n).natTrailingDegree = 0
<VAR>R : Type u<VAR>Semiring R<GOAL>Polynomial.nextCoeffUp 0 = 0
<VAR>R : Type u<VAR>Semiring R<VAR>c : R<GOAL>(Polynomial.C c).nextCoeffUp = 0
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>hp : p.coeff 0 = 0<GOAL>p.nextCoeffUp = p.coeff (p.natTrailingDegree + 1)
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<VAR>h : p.trailingDegree < q.trailingDegree<GOAL>q.coeff p.natTrailingDegree = 0
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ∞<VAR>h : p.trailingDegree < n<GOAL>p ≠ 0
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>h : Polynomial.constantCoeff p ≠ 0<GOAL>p.natTrailingDegree = 0
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>h₁ : p.Monic<GOAL>p = Polynomial.X ^ p.natDegree ↔ p.natDegree ≤ p.natTrailingDegree
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>h₁ : p.Monic<GOAL>p = Polynomial.X ^ p.natDegree ↔ p.natTrailingDegree = p.natDegree
<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>D : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} D<VAR>E : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} E<VAR>F : CategoryTheory.Functor C (CategoryTheory.Functor D E)<VAR>X : C × D<GOAL>(CategoryTheory.uncurry.obj F).obj X = (F.obj X.1).obj X.2
<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>D : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} D<VAR>E : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} E<VAR>F : CategoryTheory.Functor C (CategoryTheory.Functor D E)<VAR>X Y : C × D<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.uncurry.obj F).map f = CategoryTheory.CategoryStruct.comp ((F.map f.1).app X.2) ((F.obj Y.1).map f.2)
<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>D : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} D<VAR>E : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} E<GOAL>∀ {X Y : CategoryTheory.Functor C (CategoryTheory.Functor D E)} (T : X ⟶ Y) (X_1 : C × D), (CategoryTheory.uncurry.map T).app X_1 = (T.app X_1.1).app X_1.2
<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>D : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} D<VAR>E : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} E<VAR>F : CategoryTheory.Functor (C × D) E<GOAL>∀ {X Y : C} (f : X ⟶ Y) (Y_1 : D), ((CategoryTheory.curry.obj F).map f).app Y_1 = F.map (f, CategoryTheory.CategoryStruct.id Y_1)
<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>D : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} D<VAR>E : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} E<VAR>F : CategoryTheory.Functor (C × D) E<VAR>X : C<VAR>Y : D<GOAL>((CategoryTheory.curry.obj F).obj X).obj Y = F.obj (X, Y)
<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>D : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} D<VAR>E : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} E<VAR>F : CategoryTheory.Functor (C × D) E<VAR>X : C<GOAL>∀ {X_1 Y : D} (g : X_1 ⟶ Y), ((CategoryTheory.curry.obj F).obj X).map g = F.map (CategoryTheory.CategoryStruct.id X, g)
<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>D : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} D<VAR>E : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} E<GOAL>∀ {X Y : CategoryTheory.Functor (C × D) E} (T : X ⟶ Y) (X_1 : C) (Y_1 : D), ((CategoryTheory.curry.map T).app X_1).app Y_1 = T.app (X_1, Y_1)
<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>D : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} D<VAR>E : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} E<VAR>X : CategoryTheory.Functor C (CategoryTheory.Functor D E)<GOAL>∀ (X_1 : C) (X_2 : D), ((CategoryTheory.currying.unitIso.hom.app X).app X_1).app X_2 = CategoryTheory.CategoryStruct.id ((X.obj X_1).obj X_2)
<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>D : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} D<VAR>E : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} E<VAR>F : CategoryTheory.Functor (C × D) E<GOAL>∀ {X Y : C} (f : X ⟶ Y) (Y_1 : D), ((CategoryTheory.currying.inverse.obj F).map f).app Y_1 = F.map (f, CategoryTheory.CategoryStruct.id Y_1)
<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>D : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} D<VAR>E : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} E<VAR>X : CategoryTheory.Functor C (CategoryTheory.Functor D E)<GOAL>∀ (X_1 : C) (X_2 : D), ((CategoryTheory.currying.unitIso.inv.app X).app X_1).app X_2 = CategoryTheory.CategoryStruct.id ((X.obj X_1).obj X_2)
<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>D : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} D<VAR>E : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} E<VAR>F : CategoryTheory.Functor C (CategoryTheory.Functor D E)<VAR>X : C × D<GOAL>(CategoryTheory.currying.functor.obj F).obj X = (F.obj X.1).obj X.2
<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>D : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} D<VAR>E : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} E<VAR>X : CategoryTheory.Functor (C × D) E<GOAL>∀ (X_1 : C × D), (CategoryTheory.currying.counitIso.inv.app X).app X_1 = CategoryTheory.CategoryStruct.id (X.obj (X_1.1, X_1.2))
<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>D : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} D<VAR>E : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} E<VAR>F : CategoryTheory.Functor C (CategoryTheory.Functor D E)<VAR>X Y : C × D<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.currying.functor.obj F).map f = CategoryTheory.CategoryStruct.comp ((F.map f.1).app X.2) ((F.obj Y.1).map f.2)
<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>D : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} D<VAR>E : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} E<GOAL>∀ {X Y : CategoryTheory.Functor C (CategoryTheory.Functor D E)} (T : X ⟶ Y) (X_1 : C × D), (CategoryTheory.currying.functor.map T).app X_1 = (T.app X_1.1).app X_1.2
<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>D : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} D<VAR>E : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} E<VAR>F : CategoryTheory.Functor (C × D) E<VAR>X : C<VAR>Y : D<GOAL>((CategoryTheory.currying.inverse.obj F).obj X).obj Y = F.obj (X, Y)
<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>D : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} D<VAR>E : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} E<VAR>F : CategoryTheory.Functor (C × D) E<VAR>X : C<GOAL>∀ {X_1 Y : D} (g : X_1 ⟶ Y), ((CategoryTheory.currying.inverse.obj F).obj X).map g = F.map (CategoryTheory.CategoryStruct.id X, g)
<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>D : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} D<VAR>E : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} E<GOAL>∀ {X Y : CategoryTheory.Functor (C × D) E} (T : X ⟶ Y) (X_1 : C) (Y_1 : D), ((CategoryTheory.currying.inverse.map T).app X_1).app Y_1 = T.app (X_1, Y_1)
<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>D : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} D<VAR>E : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} E<VAR>X : CategoryTheory.Functor (C × D) E<GOAL>∀ (X_1 : C × D), (CategoryTheory.currying.counitIso.hom.app X).app X_1 = CategoryTheory.CategoryStruct.id (X.obj (X_1.1, X_1.2))
<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>D : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} D<VAR>E : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} E<VAR>F : CategoryTheory.Functor C (CategoryTheory.Functor D E)<VAR>X : D<GOAL>∀ (X_1 : C), ((CategoryTheory.flipIsoCurrySwapUncurry F).hom.app X).app X_1 = CategoryTheory.CategoryStruct.id ((F.obj X_1).obj X)
<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>D : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} D<VAR>E : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} E<VAR>F : CategoryTheory.Functor C (CategoryTheory.Functor D E)<VAR>X : D<GOAL>∀ (X_1 : C), ((CategoryTheory.flipIsoCurrySwapUncurry F).inv.app X).app X_1 = CategoryTheory.CategoryStruct.id ((F.obj X_1).obj X)
<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>D : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} D<VAR>E : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} E<VAR>F : CategoryTheory.Functor C (CategoryTheory.Functor D E)<VAR>X : D × C<GOAL>(CategoryTheory.uncurryObjFlip F).hom.app X = CategoryTheory.CategoryStruct.id ((F.obj X.2).obj X.1)
<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>D : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} D<VAR>E : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} E<VAR>F : CategoryTheory.Functor C (CategoryTheory.Functor D E)<VAR>X : D × C<GOAL>(CategoryTheory.uncurryObjFlip F).inv.app X = CategoryTheory.CategoryStruct.id ((F.obj X.2).obj X.1)
<VAR>B : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} B<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>D : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} D<VAR>E : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} E<VAR>X : CategoryTheory.Functor C (CategoryTheory.Functor D E)<GOAL>∀ (X_1 : CategoryTheory.Functor B C) (Y : CategoryTheory.Functor B D) {X_2 Y_1 : B} (f : X_2 ⟶ Y_1), ((((CategoryTheory.whiskeringRight₂ B C D E).obj X).obj X_1).obj Y).map f = CategoryTheory.CategoryStruct.comp ((X.map (X_1.map f)).app (Y.obj X_2)) ((X.obj (X_1.obj Y_1)).map (Y.map f))
<VAR>B : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} B<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>D : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} D<VAR>E : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} E<GOAL>∀ {X Y : CategoryTheory.Functor C (CategoryTheory.Functor D E)} (f : X ⟶ Y) (X_1 : CategoryTheory.Functor B C) (Y_1 : CategoryTheory.Functor B D) (c : B), ((((CategoryTheory.whiskeringRight₂ B C D E).map f).app X_1).app Y_1).app c = (f.app (X_1.obj c)).app (Y_1.obj c)
<VAR>B : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} B<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>D : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} D<VAR>E : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} E<VAR>X : CategoryTheory.Functor C (CategoryTheory.Functor D E)<GOAL>∀ {X_1 Y : CategoryTheory.Functor B C} (f : X_1 ⟶ Y) (Y_1 : CategoryTheory.Functor B D) (X_2 : B), ((((CategoryTheory.whiskeringRight₂ B C D E).obj X).map f).app Y_1).app X_2 = (X.map (f.app X_2)).app (Y_1.obj X_2)
<VAR>B : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} B<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>D : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} D<VAR>E : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} E<VAR>X : CategoryTheory.Functor C (CategoryTheory.Functor D E)<GOAL>∀ (X_1 : CategoryTheory.Functor B C) {X_2 Y : CategoryTheory.Functor B D} (g : X_2 ⟶ Y) (X_3 : B), ((((CategoryTheory.whiskeringRight₂ B C D E).obj X).obj X_1).map g).app X_3 = (X.obj (X_1.obj X_3)).map (g.app X_3)
<VAR>B : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} B<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>D : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} D<VAR>E : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} E<VAR>X : CategoryTheory.Functor C (CategoryTheory.Functor D E)<GOAL>∀ (X_1 : CategoryTheory.Functor B C) (Y : CategoryTheory.Functor B D) (X_2 : B), ((((CategoryTheory.whiskeringRight₂ B C D E).obj X).obj X_1).obj Y).obj X_2 = (X.obj (X_1.obj X_2)).obj (Y.obj X_2)
<VAR>B : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} B<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>D : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} D<VAR>F : CategoryTheory.Functor (B × C) D<GOAL>CategoryTheory.uncurry.obj (CategoryTheory.curry.obj F) = F
<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>D : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} D<VAR>E : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} E<VAR>F₁ F₂ : CategoryTheory.Functor (C × D) E<VAR>h : CategoryTheory.curry.obj F₁ = CategoryTheory.curry.obj F₂<GOAL>F₁ = F₂
<VAR>B : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} B<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>D : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} D<VAR>F : CategoryTheory.Functor B (CategoryTheory.Functor C D)<GOAL>CategoryTheory.curry.obj (CategoryTheory.uncurry.obj F) = F
<VAR>B : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} B<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>D : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} D<VAR>F₁ F₂ : CategoryTheory.Functor B (CategoryTheory.Functor C D)<VAR>h : CategoryTheory.uncurry.obj F₁ = CategoryTheory.uncurry.obj F₂<GOAL>F₁ = F₂
<VAR>B : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} B<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>D : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} D<VAR>F : CategoryTheory.Functor B (CategoryTheory.Functor C D)<GOAL>F.flip.flip = F
<VAR>B : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} B<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>D : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} D<VAR>F₁ F₂ : CategoryTheory.Functor B (CategoryTheory.Functor C D)<VAR>h : F₁.flip = F₂.flip<GOAL>F₁ = F₂
<VAR>B : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} B<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>D : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} D<VAR>E : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} E<VAR>H : Type u₅<VAR>CategoryTheory.Category.{v₅, u₅} H<VAR>F₁ : CategoryTheory.Functor B C<VAR>F₂ : CategoryTheory.Functor D E<VAR>G : CategoryTheory.Functor (C × E) H<GOAL>CategoryTheory.uncurry.obj (F₂.comp (F₁.comp (CategoryTheory.curry.obj G)).flip).flip = (F₁.prod F₂).comp G
<VAR>B : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} B<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>D : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} D<VAR>E : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} E<VAR>H : Type u₅<VAR>CategoryTheory.Category.{v₅, u₅} H<VAR>F₁ : CategoryTheory.Functor B C<VAR>F₂ : CategoryTheory.Functor D E<VAR>G : CategoryTheory.Functor (C × E) H<GOAL>CategoryTheory.uncurry.obj (F₁.comp (F₂.comp (CategoryTheory.curry.obj G).flip).flip) = (F₁.prod F₂).comp G
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>Semiring R<VAR>CommSemiring K<VAR>i : R →+* K<VAR>b : R<VAR>bi : K<VAR>N : ℕ<VAR>a : R<VAR>bu : bi * i b = 1<GOAL>DenomsClearable a b N 0 i
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>Semiring R<VAR>CommSemiring K<VAR>i : R →+* K<VAR>b : R<VAR>bi : K<VAR>N : ℕ<VAR>a : R<VAR>bu : bi * i b = 1<VAR>n : ℕ<VAR>r : R<VAR>nN : n ≤ N<GOAL>DenomsClearable a b N (Polynomial.C r * Polynomial.X ^ n) i
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>Semiring R<VAR>CommSemiring K<VAR>i : R →+* K<VAR>a b : R<VAR>N : ℕ<VAR>f g : R[X]<GOAL>DenomsClearable a b N f i → DenomsClearable a b N g i → DenomsClearable a b N (f + g) i
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>Semiring R<VAR>CommSemiring K<VAR>i : R →+* K<VAR>b : R<VAR>bi : K<VAR>N : ℕ<VAR>a : R<VAR>bu : bi * i b = 1<VAR>f : R[X]<GOAL>f.natDegree ≤ N → DenomsClearable a b N f i
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>Semiring R<VAR>CommSemiring K<VAR>b : R<VAR>bi : K<VAR>i : R →+* K<VAR>f : R[X]<VAR>a : R<VAR>bu : bi * i b = 1<GOAL>DenomsClearable a b f.natDegree f i
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>f : ℤ[X]<VAR>a b : ℤ<VAR>b0 : 0 < b<VAR>fab : Polynomial.eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0<GOAL>1 ≤ ↑b ^ f.natDegree * |Polynomial.eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f)|
<VAR>Fq : Type u_1<VAR>Field Fq<VAR>Fintype Fq<VAR>DecidableEq Fq<VAR>p : Polynomial Fq<GOAL>Polynomial.cardPowDegree p = if p = 0 then 0 else ↑(Fintype.card Fq) ^ p.natDegree
<VAR>Fq : Type u_1<VAR>Field Fq<VAR>Fintype Fq<GOAL>Polynomial.cardPowDegree 0 = 0
<VAR>Fq : Type u_1<VAR>Field Fq<VAR>Fintype Fq<VAR>p : Polynomial Fq<VAR>hp : p ≠ 0<GOAL>Polynomial.cardPowDegree p = ↑(Fintype.card Fq) ^ p.natDegree
<VAR>Fq : Type u_1<VAR>Field Fq<VAR>Fintype Fq<GOAL>Polynomial.cardPowDegree.IsEuclidean
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<GOAL>(p.comp q).natDegree ≤ p.natDegree * q.natDegree
<VAR>R : Type u<VAR>a : R<VAR>Semiring R<VAR>p : R[X]<VAR>hp : p ≠ 0<VAR>h : p.IsRoot a<GOAL>0 < p.degree
<VAR>R : Type u<VAR>n : ℕ<VAR>Semiring R<VAR>p : R[X]<GOAL>p.natDegree ≤ n ↔ ∀ (N : ℕ), n < N → p.coeff N = 0
<VAR>R : Type u<VAR>Semiring R<VAR>n : ℕ<VAR>p q : R[X]<VAR>qn : q.natDegree ≤ n<GOAL>(p + q).natDegree ≤ n ↔ p.natDegree ≤ n
<VAR>R : Type u<VAR>Semiring R<VAR>n : ℕ<VAR>p q : R[X]<VAR>pn : p.natDegree ≤ n<GOAL>(p + q).natDegree ≤ n ↔ q.natDegree ≤ n
<VAR>R : Type u<VAR>Semiring R<VAR>a : R<VAR>f : R[X]<GOAL>(Polynomial.C a * f).natDegree ≤ f.natDegree
<VAR>R : Type u<VAR>Semiring R<VAR>f : R[X]<VAR>a : R<GOAL>(f * Polynomial.C a).natDegree ≤ f.natDegree
<VAR>R : Type u<VAR>n : ℕ<VAR>Semiring R<VAR>p : R[X]<VAR>pn : p.natDegree ≤ n<VAR>ns : n ∈ p.support<GOAL>p.natDegree = n
<VAR>R : Type u<VAR>a : R<VAR>Semiring R<VAR>p : R[X]<VAR>ai : R<VAR>au : ai * a = 1<GOAL>(Polynomial.C a * p).natDegree = p.natDegree
<VAR>R : Type u<VAR>a : R<VAR>Semiring R<VAR>p : R[X]<VAR>ai : R<VAR>au : a * ai = 1<GOAL>(p * Polynomial.C a).natDegree = p.natDegree
<VAR>R : Type u<VAR>a : R<VAR>Semiring R<VAR>p : R[X]<VAR>h : p.leadingCoeff * a ≠ 0<GOAL>(p * Polynomial.C a).natDegree = p.natDegree
<VAR>R : Type u<VAR>a : R<VAR>Semiring R<VAR>p : R[X]<VAR>h : a * p.leadingCoeff ≠ 0<GOAL>(Polynomial.C a * p).natDegree = p.natDegree
<VAR>R : Type u<VAR>Semiring R<VAR>f g : R[X]<GOAL>(f * g).coeff (f.natDegree + g.natDegree) = f.coeff f.natDegree * g.coeff g.natDegree
<VAR>R : Type u<VAR>m n : ℕ<VAR>Semiring R<VAR>p q : R[X]<VAR>h : p.natDegree + q.natDegree < m + n<GOAL>(p * q).coeff (m + n) = 0
<VAR>R : Type u<VAR>m n : ℕ<VAR>Semiring R<VAR>p q : R[X]<VAR>pm : p.natDegree ≤ m<VAR>qn : q.natDegree ≤ n<GOAL>(p * q).coeff (m + n) = p.coeff m * q.coeff n
<VAR>R : Type u<VAR>m n : ℕ<VAR>Semiring R<VAR>p : R[X]<VAR>pn : p.natDegree ≤ n<GOAL>(p ^ m).coeff (m * n) = p.coeff n ^ m
<VAR>R : Type u<VAR>m n : ℕ<VAR>Semiring R<VAR>p : R[X]<VAR>o : ℕ<VAR>pn : p.natDegree ≤ n<VAR>mno : m * n ≤ o<GOAL>(p ^ m).coeff o = if o = m * n then p.coeff n ^ m else 0
<VAR>R : Type u<VAR>n : ℕ<VAR>Semiring R<VAR>p q : R[X]<VAR>qn : q.natDegree < n<GOAL>(p + q).coeff n = p.coeff n
<VAR>R : Type u<VAR>n : ℕ<VAR>Semiring R<VAR>p q : R[X]<VAR>pn : p.natDegree < n<GOAL>(p + q).coeff n = q.coeff n
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>f : S → R[X]<VAR>s : Finset S<VAR>h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on Polynomial.degree ∘ f)<GOAL>(s.sum f).degree = s.sup fun i => (f i).degree
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>f : S → R[X]<VAR>s : Finset S<VAR>h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on Polynomial.natDegree ∘ f)<GOAL>(s.sum f).natDegree = s.sup fun i => (f i).natDegree
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>p : R[X]<VAR>hp : p ≠ 0<VAR>f : R →+* S<VAR>z : S<VAR>hz : Polynomial.eval₂ f z p = 0<VAR>inj : ∀ (x : R), f x = 0 → x = 0<GOAL>0 < p.natDegree
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>p : R[X]<VAR>hp : p ≠ 0<VAR>f : R →+* S<VAR>z : S<VAR>hz : Polynomial.eval₂ f z p = 0<VAR>inj : ∀ (x : R), f x = 0 → x = 0<GOAL>0 < p.degree
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ<GOAL>↑n < p.degree ↔ n < p.natDegree
<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 ↔ f p.leadingCoeff ≠ 0 ∨ p = 0
<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 ↔ f p.leadingCoeff ≠ 0 ∨ p.natDegree = 0
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>h : p.nextCoeff ≠ 0<GOAL>0 < p.natDegree
<VAR>R : Type u<VAR>Ring R<VAR>p q : R[X]<GOAL>(p - q).natDegree = (q - p).natDegree
<VAR>R : Type u<VAR>n : ℕ<VAR>Ring R<VAR>p q : R[X]<VAR>qn : q.natDegree ≤ n<GOAL>(p - q).natDegree ≤ n ↔ p.natDegree ≤ n
<VAR>R : Type u<VAR>n : ℕ<VAR>Ring R<VAR>p q : R[X]<VAR>pn : p.natDegree ≤ n<GOAL>(p - q).natDegree ≤ n ↔ q.natDegree ≤ n
<VAR>R : Type u<VAR>n : ℕ<VAR>Ring R<VAR>p q : R[X]<VAR>dg : q.natDegree < n<GOAL>(p - q).coeff n = p.coeff n
<VAR>R : Type u<VAR>n : ℕ<VAR>Ring R<VAR>p q : R[X]<VAR>df : p.natDegree < n<GOAL>(p - q).coeff n = -q.coeff n
<VAR>R : Type u<VAR>Semiring R<VAR>NoZeroDivisors R<VAR>p : R[X]<VAR>a : R<VAR>a0 : a ≠ 0<GOAL>(p * Polynomial.C a).degree = p.degree
<VAR>R : Type u<VAR>Semiring R<VAR>NoZeroDivisors R<VAR>p : R[X]<VAR>a : R<VAR>a0 : a ≠ 0<GOAL>(Polynomial.C a * p).degree = p.degree
<VAR>R : Type u<VAR>Semiring R<VAR>NoZeroDivisors R<VAR>p : R[X]<VAR>a : R<VAR>a0 : a ≠ 0<GOAL>(p * Polynomial.C a).natDegree = p.natDegree
<VAR>R : Type u<VAR>Semiring R<VAR>NoZeroDivisors R<VAR>p : R[X]<VAR>a : R<VAR>a0 : a ≠ 0<GOAL>(Polynomial.C a * p).natDegree = p.natDegree
<VAR>R : Type u<VAR>Semiring R<VAR>a : R<VAR>ha : a ≠ 0<VAR>c : R<GOAL>(Polynomial.C a * Polynomial.X + Polynomial.C c).nextCoeff = c
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>p.natDegree = 1 ↔ ∃ a, a ≠ 0 ∧ ∃ b, Polynomial.C a * Polynomial.X + Polynomial.C b = p
<VAR>R : Type u<VAR>Semiring R<VAR>NoZeroDivisors R<VAR>p q : R[X]<GOAL>(p.comp q).natDegree = p.natDegree * q.natDegree
<VAR>R : Type u<VAR>Semiring R<VAR>NoZeroDivisors R<VAR>p q : R[X]<VAR>k : ℕ<GOAL>(p.comp^[k] q).natDegree = p.natDegree ^ k * q.natDegree
<VAR>R : Type u<VAR>Semiring R<VAR>NoZeroDivisors R<VAR>p q : R[X]<VAR>hq : q.natDegree ≠ 0<GOAL>(p.comp q).leadingCoeff = p.leadingCoeff * q.leadingCoeff ^ p.natDegree
<VAR>K : Type u_1<VAR>DivisionRing K<VAR>p : K[X]<GOAL>Irreducible (p * Polynomial.C p.leadingCoeff⁻¹) ↔ Irreducible p
<VAR>K : Type u_1<VAR>DivisionRing K<VAR>p q : K[X]<VAR>hp0 : p ≠ 0<GOAL>q ∣ p * Polynomial.C p.leadingCoeff⁻¹ ↔ q ∣ p
<VAR>K : Type u_1<VAR>DivisionRing K<VAR>p : K[X]<VAR>h : p ≠ 0<GOAL>(p * Polynomial.C p.leadingCoeff⁻¹).Monic
<VAR>K : Type u_1<VAR>DivisionRing K<VAR>p : K[X]<VAR>hp0 : p ≠ 0<GOAL>(Polynomial.C p.leadingCoeff⁻¹).degree = 0
<VAR>K : Type u_1<VAR>DivisionRing K<VAR>p : K[X]<VAR>q : K[X]<VAR>h : q ≠ 0<GOAL>(p * Polynomial.C q.leadingCoeff⁻¹).degree = p.degree
<VAR>K : Type u_1<VAR>DivisionRing K<VAR>p : K[X]<VAR>q : K[X]<VAR>h : q ≠ 0<GOAL>(p * Polynomial.C q.leadingCoeff⁻¹).natDegree = p.natDegree
<VAR>K : Type u_1<VAR>DivisionRing K<VAR>p : K[X]<GOAL>(p * Polynomial.C p.leadingCoeff⁻¹).degree = p.degree
<VAR>K : Type u_1<VAR>DivisionRing K<VAR>p : K[X]<GOAL>(p * Polynomial.C p.leadingCoeff⁻¹).natDegree = p.natDegree
<VAR>K : Type u_1<VAR>DivisionRing K<VAR>p : K[X]<GOAL>p.degree + (Polynomial.C p.leadingCoeff⁻¹).degree = p.degree
<VAR>R : Type u<VAR>n : ℕ<VAR>Semiring R<VAR>p : R[X]<GOAL>p.divX.coeff n = p.coeff (n + 1)
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>p.divX * Polynomial.X + Polynomial.C (p.coeff 0) = p
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>Polynomial.X * p.divX + Polynomial.C (p.coeff 0) = p
<VAR>R : Type u<VAR>Semiring R<VAR>a : R<GOAL>(Polynomial.C a).divX = 0
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>p.divX = 0 ↔ p = Polynomial.C (p.coeff 0)
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<GOAL>(p + q).divX = p.divX + q.divX
<VAR>R : Type u<VAR>Semiring R<GOAL>Polynomial.divX 0 = 0
<VAR>R : Type u<VAR>Semiring R<GOAL>Polynomial.divX 1 = 0
<VAR>R : Type u<VAR>a : R<VAR>Semiring R<VAR>p : R[X]<GOAL>(Polynomial.C a * p).divX = Polynomial.C a * p.divX
<VAR>R : Type u<VAR>n : ℕ<VAR>Semiring R<GOAL>(Polynomial.X ^ n).divX = if n = 0 then 0 else Polynomial.X ^ (n - 1)
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>Polynomial.divX_hom p = p.divX
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>p.divX.natDegree = p.natDegree - 1
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>p.divX.natDegree ≤ p.natDegree
<VAR>R : Type u<VAR>a : R<VAR>n : ℕ<VAR>Semiring R<GOAL>(Polynomial.C a * Polynomial.X ^ n).divX = if n = 0 then 0 else Polynomial.C a * Polynomial.X ^ (n - 1)
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>hp0 : p ≠ 0<GOAL>p.divX.degree < p.degree