ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>Nontrivial S<VAR>P : R[X]<VAR>hmo : P.Monic<VAR>f : R →+* S<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>hf : Function.Injective ⇑f<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>hf : Function.Injective ⇑f<VAR>p : R[X]<GOAL>(Polynomial.map f p).natDegree = p.natDegree
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>hf : Function.Injective ⇑f<VAR>p : R[X]<GOAL>(Polynomial.map f p).leadingCoeff = f p.leadingCoeff
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>hf : Function.Injective ⇑f<VAR>p : R[X]<GOAL>(Polynomial.map f p).nextCoeff = f p.nextCoeff
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>hf : Function.Injective ⇑f<VAR>p : R[X]<VAR>hp : (Polynomial.map f p).Monic<GOAL>p.Monic
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>hf : Function.Injective ⇑f<VAR>p : R[X]<GOAL>p.Monic ↔ (Polynomial.map f p).Monic
<VAR>R : Type u<VAR>Ring R<VAR>x : R<GOAL>(Polynomial.X - Polynomial.C x).Monic
<VAR>R : Type u<VAR>Ring R<VAR>p : R[X]<VAR>n : ℕ<VAR>H : p.degree ≤ ↑n<GOAL>(Polynomial.X ^ (n + 1) - p).Monic
<VAR>R : Type u<VAR>Ring R<VAR>a : R<VAR>n : ℕ<VAR>h : n ≠ 0<GOAL>(Polynomial.X ^ n - Polynomial.C a).Monic
<VAR>R : Type u_1<VAR>CommRing R<VAR>Nontrivial R<VAR>n : ℕ<GOAL>¬IsUnit (Polynomial.X ^ n - 1)
<VAR>R : Type u<VAR>Ring R<VAR>p q : R[X]<VAR>hp : p.Monic<VAR>hpq : q.degree < p.degree<GOAL>(p - q).Monic
<VAR>R : Type u<VAR>Ring R<VAR>p q : R[X]<VAR>hq : q.leadingCoeff = -1<VAR>hpq : p.degree < q.degree<GOAL>(p - q).Monic
<VAR>R : Type u<VAR>Semiring R<VAR>Nontrivial R<GOAL>¬Polynomial.Monic 0
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>hp : p.Monic<VAR>q : R[X]<VAR>hq : q ≠ 0<GOAL>q * p ≠ 0
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>hp : p.Monic<VAR>q : R[X]<VAR>hq : q ≠ 0<GOAL>p * q ≠ 0
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>h : p.Monic<VAR>q : R[X]<GOAL>(p * q).natDegree < p.natDegree ↔ p ≠ 1 ∧ q = 0
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>h : p.Monic<VAR>q : R[X]<GOAL>p * q = 0 ↔ q = 0
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>h : p.Monic<VAR>q : R[X]<GOAL>q * p = 0 ↔ q = 0
<VAR>R : Type u_1<VAR>Ring R<VAR>p : R[X]<VAR>hp : p.Monic<GOAL>IsRegular p
<VAR>R : Type u<VAR>Semiring R<VAR>S : Type u_1<VAR>Monoid S<VAR>DistribMulAction S R<VAR>k : S<VAR>p : R[X]<VAR>h : IsSMulRegular R k<GOAL>(k • p).degree = p.degree
<VAR>R : Type u<VAR>Semiring R<VAR>S : Type u_1<VAR>Monoid S<VAR>DistribMulAction S R<VAR>k : S<VAR>p : R[X]<VAR>h : IsSMulRegular R k<GOAL>(k • p).natDegree = p.natDegree
<VAR>R : Type u<VAR>Semiring R<VAR>S : Type u_1<VAR>Monoid S<VAR>DistribMulAction S R<VAR>k : S<VAR>p : R[X]<VAR>h : IsSMulRegular R k<GOAL>(k • p).leadingCoeff = k • p.leadingCoeff
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>h : IsUnit p.leadingCoeff<GOAL>(h.unit⁻¹ • p).Monic
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>h : IsUnit p.leadingCoeff<VAR>q : R[X]<GOAL>p * q = 0 ↔ q = 0
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>h : IsUnit p.leadingCoeff<VAR>q : R[X]<GOAL>q * p = 0 ↔ q = 0
<VAR>R : Type u_1<VAR>Ring R<VAR>a b c : R<GOAL>discrim (-a) (-b) (-c) = discrim a b c
<VAR>R : Type u_1<VAR>CommRing R<VAR>a b c x : R<VAR>h : a * x * x + b * x + c = 0<GOAL>discrim a b c = (2 * a * x + b) ^ 2
<VAR>R : Type u_1<VAR>CommRing R<VAR>a b c : R<VAR>NeZero 2<VAR>NoZeroDivisors R<VAR>ha : a ≠ 0<VAR>x : R<GOAL>a * x * x + b * x + c = 0 ↔ discrim a b c = (2 * a * x + b) ^ 2
<VAR>R : Type u_1<VAR>CommRing R<VAR>a b c : R<VAR>h : ∀ (s : R), discrim a b c ≠ s ^ 2<VAR>x : R<GOAL>a * x * x + b * x + c ≠ 0
<VAR>K : Type u_1<VAR>Field K<VAR>NeZero 2<VAR>a b c : K<VAR>ha : a ≠ 0<VAR>s : K<VAR>h : discrim a b c = s * s<VAR>x : K<GOAL>a * x * x + b * x + c = 0 ↔ x = (-b + s) / (2 * a) ∨ x = (-b - s) / (2 * a)
<VAR>K : Type u_1<VAR>Field K<VAR>NeZero 2<VAR>a b c : K<VAR>ha : a ≠ 0<VAR>h : ∃ s, discrim a b c = s * s<GOAL>∃ x, a * x * x + b * x + c = 0
<VAR>K : Type u_1<VAR>Field K<VAR>NeZero 2<VAR>a b c : K<VAR>ha : a ≠ 0<VAR>h : discrim a b c = 0<VAR>x : K<GOAL>a * x * x + b * x + c = 0 ↔ x = -b / (2 * a)
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>a b c : K<VAR>h : ∀ (x : K), 0 ≤ a * x * x + b * x + c<GOAL>discrim a b c ≤ 0
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>a b c : K<VAR>h : ∀ (x : K), a * x * x + b * x + c ≤ 0<GOAL>discrim a b c ≤ 0
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>a b c : K<VAR>ha : a ≠ 0<VAR>h : ∀ (x : K), 0 < a * x * x + b * x + c<GOAL>discrim a b c < 0
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>a b c : K<VAR>ha : a ≠ 0<VAR>h : ∀ (x : K), a * x * x + b * x + c < 0<GOAL>discrim a b c < 0
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>NonAssocSemiring α<VAR>Preorder α<VAR>NonAssocSemiring β<VAR>Preorder β<VAR>self : α →+*o β<GOAL>Monotone (↑↑self.toRingHom).toFun
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>Mul α<VAR>Mul β<VAR>Add α<VAR>Add β<VAR>LE α<VAR>LE β<VAR>self : α ≃+*o β<VAR>a b : α<GOAL>self.toFun a ≤ self.toFun b ↔ a ≤ b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>NonAssocSemiring α<VAR>Preorder α<VAR>NonAssocSemiring β<VAR>Preorder β<VAR>f : α →+*o β<GOAL>(↑↑f.toRingHom).toFun = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>NonAssocSemiring α<VAR>Preorder α<VAR>NonAssocSemiring β<VAR>Preorder β<VAR>f g : α →+*o β<VAR>h : ∀ (a : α), f a = g a<GOAL>f = g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>NonAssocSemiring α<VAR>Preorder α<VAR>NonAssocSemiring β<VAR>Preorder β<VAR>f : α →+*o β<GOAL>f.toRingHom = ↑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>NonAssocSemiring α<VAR>Preorder α<VAR>NonAssocSemiring β<VAR>Preorder β<VAR>f : α →+*o β<GOAL>f.toOrderAddMonoidHom = ↑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>NonAssocSemiring α<VAR>Preorder α<VAR>NonAssocSemiring β<VAR>Preorder β<VAR>f : α →+*o β<GOAL>f.toOrderMonoidWithZeroHom = ↑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>NonAssocSemiring α<VAR>Preorder α<VAR>NonAssocSemiring β<VAR>Preorder β<VAR>f : α →+*o β<GOAL>⇑↑f = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>NonAssocSemiring α<VAR>Preorder α<VAR>NonAssocSemiring β<VAR>Preorder β<VAR>f : α →+*o β<VAR>a : α<GOAL>↑f a = f a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>NonAssocSemiring α<VAR>Preorder α<VAR>NonAssocSemiring β<VAR>Preorder β<VAR>f : α →+*o β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>⇑(f.copy f' h) = f'
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>NonAssocSemiring α<VAR>Preorder α<VAR>NonAssocSemiring β<VAR>Preorder β<VAR>f : α →+*o β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>f.copy f' h = f
<VAR>α : Type u_2<VAR>NonAssocSemiring α<VAR>Preorder α<GOAL>⇑(OrderRingHom.id α) = id
<VAR>α : Type u_2<VAR>NonAssocSemiring α<VAR>Preorder α<VAR>a : α<GOAL>(OrderRingHom.id α) a = a
<VAR>α : Type u_2<VAR>NonAssocSemiring α<VAR>Preorder α<GOAL>↑(OrderRingHom.id α) = RingHom.id α
<VAR>α : Type u_2<VAR>NonAssocSemiring α<VAR>Preorder α<GOAL>↑(OrderRingHom.id α) = OrderAddMonoidHom.id α
<VAR>α : Type u_2<VAR>NonAssocSemiring α<VAR>Preorder α<GOAL>↑(OrderRingHom.id α) = OrderMonoidWithZeroHom.id α
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>NonAssocSemiring α<VAR>Preorder α<VAR>NonAssocSemiring β<VAR>Preorder β<VAR>NonAssocSemiring γ<VAR>Preorder γ<VAR>f : β →+*o γ<VAR>g : α →+*o β<GOAL>⇑(f.comp g) = ⇑f ∘ ⇑g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>NonAssocSemiring α<VAR>Preorder α<VAR>NonAssocSemiring β<VAR>Preorder β<VAR>NonAssocSemiring γ<VAR>Preorder γ<VAR>f : β →+*o γ<VAR>g : α →+*o β<VAR>a : α<GOAL>(f.comp g) a = f (g a)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>NonAssocSemiring α<VAR>Preorder α<VAR>NonAssocSemiring β<VAR>Preorder β<VAR>NonAssocSemiring γ<VAR>Preorder γ<VAR>NonAssocSemiring δ<VAR>Preorder δ<VAR>f : γ →+*o δ<VAR>g : β →+*o γ<VAR>h : α →+*o β<GOAL>(f.comp g).comp h = f.comp (g.comp h)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>NonAssocSemiring α<VAR>Preorder α<VAR>NonAssocSemiring β<VAR>Preorder β<VAR>f : α →+*o β<GOAL>f.comp (OrderRingHom.id α) = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>NonAssocSemiring α<VAR>Preorder α<VAR>NonAssocSemiring β<VAR>Preorder β<VAR>f : α →+*o β<GOAL>(OrderRingHom.id β).comp f = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>NonAssocSemiring α<VAR>Preorder α<VAR>NonAssocSemiring β<VAR>Preorder β<VAR>NonAssocSemiring γ<VAR>Preorder γ<VAR>f₁ f₂ : β →+*o γ<VAR>g : α →+*o β<VAR>hg : Function.Surjective ⇑g<GOAL>f₁.comp g = f₂.comp g ↔ f₁ = f₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>NonAssocSemiring α<VAR>Preorder α<VAR>NonAssocSemiring β<VAR>Preorder β<VAR>NonAssocSemiring γ<VAR>Preorder γ<VAR>f : β →+*o γ<VAR>g₁ g₂ : α →+*o β<VAR>hf : Function.Injective ⇑f<GOAL>f.comp g₁ = f.comp g₂ ↔ g₁ = g₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Mul α<VAR>Add α<VAR>LE α<VAR>Mul β<VAR>Add β<VAR>LE β<VAR>f : α ≃+*o β<GOAL>f.toFun = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Mul α<VAR>Add α<VAR>LE α<VAR>Mul β<VAR>Add β<VAR>LE β<VAR>f g : α ≃+*o β<VAR>h : ∀ (a : α), f a = g a<GOAL>f = g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Mul α<VAR>Add α<VAR>LE α<VAR>Mul β<VAR>Add β<VAR>LE β<VAR>e : α ≃+* β<VAR>h : ∀ {a b : α}, e.toFun a ≤ e.toFun b ↔ a ≤ b<GOAL>⇑{ toRingEquiv := e, map_le_map_iff' := h } = ⇑e
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Mul α<VAR>Add α<VAR>LE α<VAR>Mul β<VAR>Add β<VAR>LE β<VAR>e : α ≃+*o β<VAR>h : ∀ {a b : α}, (↑e).toFun a ≤ (↑e).toFun b ↔ a ≤ b<GOAL>{ toRingEquiv := ↑e, map_le_map_iff' := h } = e
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Mul α<VAR>Add α<VAR>LE α<VAR>Mul β<VAR>Add β<VAR>LE β<VAR>f : α ≃+*o β<GOAL>f.toRingEquiv = ↑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Mul α<VAR>Add α<VAR>LE α<VAR>Mul β<VAR>Add β<VAR>LE β<VAR>f : α ≃+*o β<GOAL>↑f = ↑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Mul α<VAR>Add α<VAR>LE α<VAR>Mul β<VAR>Add β<VAR>LE β<VAR>f : α ≃+*o β<GOAL>⇑↑f = ⇑f
<VAR>α : Type u_2<VAR>Mul α<VAR>Add α<VAR>LE α<VAR>x : α<GOAL>(OrderRingIso.refl α) x = x
<VAR>α : Type u_2<VAR>Mul α<VAR>Add α<VAR>LE α<GOAL>↑(OrderRingIso.refl α) = RingEquiv.refl α
<VAR>α : Type u_2<VAR>Mul α<VAR>Add α<VAR>LE α<GOAL>↑(OrderRingIso.refl α) = OrderIso.refl α
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Mul α<VAR>Add α<VAR>LE α<VAR>Mul β<VAR>Add β<VAR>LE β<VAR>e : α ≃+*o β<GOAL>e.symm.symm = e
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Mul α<VAR>Add α<VAR>LE α<VAR>Mul β<VAR>Add β<VAR>LE β<VAR>Mul γ<VAR>Add γ<VAR>LE γ<VAR>f : α ≃+*o β<VAR>g : β ≃+*o γ<GOAL>(f.trans g).toRingEquiv = f.trans g.toRingEquiv
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Mul α<VAR>Add α<VAR>LE α<VAR>Mul β<VAR>Add β<VAR>LE β<VAR>Mul γ<VAR>Add γ<VAR>LE γ<VAR>f : α ≃+*o β<VAR>g : β ≃+*o γ<GOAL>↑(f.trans g) = f.trans g.toRingEquiv
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Mul α<VAR>Add α<VAR>LE α<VAR>Mul β<VAR>Add β<VAR>LE β<VAR>Mul γ<VAR>Add γ<VAR>LE γ<VAR>f : α ≃+*o β<VAR>g : β ≃+*o γ<VAR>a : α<GOAL>(f.trans g) a = g (f a)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Mul α<VAR>Add α<VAR>LE α<VAR>Mul β<VAR>Add β<VAR>LE β<VAR>e : α ≃+*o β<GOAL>e.trans e.symm = OrderRingIso.refl α
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Mul α<VAR>Add α<VAR>LE α<VAR>Mul β<VAR>Add β<VAR>LE β<VAR>e : α ≃+*o β<GOAL>e.symm.trans e = OrderRingIso.refl β
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Mul α<VAR>Add α<VAR>LE α<VAR>Mul β<VAR>Add β<VAR>LE β<GOAL>Function.Bijective OrderRingIso.symm
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>NonAssocSemiring α<VAR>Preorder α<VAR>NonAssocSemiring β<VAR>Preorder β<VAR>f : α ≃+*o β<GOAL>f.toOrderRingHom = ↑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>NonAssocSemiring α<VAR>Preorder α<VAR>NonAssocSemiring β<VAR>Preorder β<VAR>f : α ≃+*o β<GOAL>⇑↑f = ⇑f
<VAR>α : Type u_2<VAR>NonAssocSemiring α<VAR>Preorder α<GOAL>↑(OrderRingIso.refl α) = OrderRingHom.id α
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>NonAssocSemiring α<VAR>Preorder α<VAR>NonAssocSemiring β<VAR>Preorder β<GOAL>Function.Injective OrderRingIso.toOrderRingHom
<VAR>R : Type u<VAR>CommSemiring R<VAR>p : ℕ<GOAL>⇑(Polynomial.expand R p) = Polynomial.eval₂ Polynomial.C (Polynomial.X ^ p)
<VAR>R : Type u<VAR>CommSemiring R<VAR>p : ℕ<VAR>f : R[X]<GOAL>(Polynomial.expand R p) f = f.comp (Polynomial.X ^ p)
<VAR>R : Type u<VAR>CommSemiring R<VAR>p : ℕ<VAR>f : R[X]<GOAL>(Polynomial.expand R p) f = f.sum fun e a => Polynomial.C a * (Polynomial.X ^ p) ^ e
<VAR>R : Type u<VAR>CommSemiring R<VAR>p : ℕ<VAR>r : R<GOAL>(Polynomial.expand R p) (Polynomial.C r) = Polynomial.C r
<VAR>R : Type u<VAR>CommSemiring R<VAR>p : ℕ<GOAL>(Polynomial.expand R p) Polynomial.X = Polynomial.X ^ p
<VAR>R : Type u<VAR>CommSemiring R<VAR>p q : ℕ<VAR>r : R<GOAL>(Polynomial.expand R p) ((Polynomial.monomial q) r) = (Polynomial.monomial (q * p)) r
<VAR>R : Type u<VAR>CommSemiring R<VAR>p q : ℕ<VAR>f : R[X]<GOAL>(Polynomial.expand R p) ((Polynomial.expand R q) f) = (Polynomial.expand R (p * q)) f
<VAR>R : Type u<VAR>CommSemiring R<VAR>p q : ℕ<VAR>f : R[X]<GOAL>(Polynomial.expand R (p * q)) f = (Polynomial.expand R p) ((Polynomial.expand R q) f)
<VAR>R : Type u<VAR>CommSemiring R<VAR>f : R[X]<GOAL>(Polynomial.expand R 0) f = Polynomial.C (Polynomial.eval 1 f)
<VAR>R : Type u<VAR>CommSemiring R<VAR>f : R[X]<GOAL>(Polynomial.expand R 1) f = f
<VAR>R : Type u<VAR>CommSemiring R<VAR>p q : ℕ<VAR>f : R[X]<GOAL>(Polynomial.expand R (p ^ q)) f = (⇑(Polynomial.expand R p))^[q] f
<VAR>R : Type u<VAR>CommSemiring R<VAR>p : ℕ<VAR>f : R[X]<GOAL>Polynomial.derivative ((Polynomial.expand R p) f) = (Polynomial.expand R p) (Polynomial.derivative f) * (↑p * Polynomial.X ^ (p - 1))
<VAR>R : Type u<VAR>CommSemiring R<VAR>p : ℕ<VAR>hp : 0 < p<VAR>f : R[X]<VAR>n : ℕ<GOAL>((Polynomial.expand R p) f).coeff n = if p ∣ n then f.coeff (n / p) else 0
<VAR>R : Type u<VAR>CommSemiring R<VAR>p : ℕ<VAR>hp : 0 < p<VAR>f : R[X]<VAR>n : ℕ<GOAL>((Polynomial.expand R p) f).coeff (n * p) = f.coeff n
<VAR>R : Type u<VAR>CommSemiring R<VAR>p : ℕ<VAR>hp : 0 < p<VAR>f : R[X]<VAR>n : ℕ<GOAL>((Polynomial.expand R p) f).coeff (p * n) = f.coeff n
<VAR>R : Type u<VAR>CommSemiring R<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>Function.Injective ⇑(Polynomial.expand R n)
<VAR>R : Type u<VAR>CommSemiring R<VAR>p : ℕ<VAR>hp : 0 < p<VAR>f g : R[X]<GOAL>(Polynomial.expand R p) f = (Polynomial.expand R p) g ↔ f = g
<VAR>R : Type u<VAR>CommSemiring R<VAR>p : ℕ<VAR>hp : 0 < p<VAR>f : R[X]<GOAL>(Polynomial.expand R p) f = 0 ↔ f = 0
<VAR>R : Type u<VAR>CommSemiring R<VAR>p : ℕ<VAR>hp : 0 < p<VAR>f : R[X]<GOAL>(Polynomial.expand R p) f ≠ 0 ↔ f ≠ 0
<VAR>R : Type u<VAR>CommSemiring R<VAR>p : ℕ<VAR>hp : 0 < p<VAR>f : R[X]<VAR>r : R<GOAL>(Polynomial.expand R p) f = Polynomial.C r ↔ f = Polynomial.C r
<VAR>R : Type u<VAR>CommSemiring R<VAR>p : ℕ<VAR>f : R[X]<GOAL>((Polynomial.expand R p) f).natDegree = f.natDegree * p
<VAR>R : Type u<VAR>CommSemiring R<VAR>p : ℕ<VAR>f : R[X]<VAR>hp : 0 < p<GOAL>((Polynomial.expand R p) f).leadingCoeff = f.leadingCoeff
<VAR>R : Type u<VAR>CommSemiring R<VAR>p : ℕ<VAR>f : R[X]<VAR>hp : 0 < p<GOAL>((Polynomial.expand R p) f).Monic ↔ f.Monic
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Type v<VAR>CommSemiring S<VAR>p : ℕ<VAR>f : R →+* S<VAR>q : R[X]<GOAL>Polynomial.map f ((Polynomial.expand R p) q) = (Polynomial.expand S p) (Polynomial.map f q)
<VAR>R : Type u<VAR>CommSemiring R<VAR>p : ℕ<VAR>P : R[X]<VAR>r : R<GOAL>Polynomial.eval r ((Polynomial.expand R p) P) = Polynomial.eval (r ^ p) P
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type u_1<VAR>Semiring A<VAR>Algebra R A<VAR>p : ℕ<VAR>P : R[X]<VAR>r : A<GOAL>(Polynomial.aeval r) ((Polynomial.expand R p) P) = (Polynomial.aeval (r ^ p)) P
<VAR>R : Type u<VAR>CommSemiring R<VAR>p : ℕ<VAR>hp : p ≠ 0<VAR>f : R[X]<VAR>n : ℕ<GOAL>(Polynomial.contract p f).coeff n = f.coeff (n * p)
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Type v<VAR>CommSemiring S<VAR>p : ℕ<VAR>hp : p ≠ 0<VAR>f : R →+* S<VAR>q : R[X]<GOAL>Polynomial.map f (Polynomial.contract p q) = Polynomial.contract p (Polynomial.map f q)
<VAR>R : Type u<VAR>CommSemiring R<VAR>p : ℕ<VAR>f : R[X]<VAR>hp : p ≠ 0<GOAL>Polynomial.contract p ((Polynomial.expand R p) f) = f
<VAR>R : Type u<VAR>CommSemiring R<VAR>f : R[X]<GOAL>Polynomial.contract 1 f = f
<VAR>R : Type u<VAR>CommSemiring R<VAR>p : ℕ<VAR>CharP R p<VAR>NoZeroDivisors R<VAR>f : R[X]<VAR>hf : Polynomial.derivative f = 0<VAR>hp : p ≠ 0<GOAL>(Polynomial.expand R p) (Polynomial.contract p f) = f
<VAR>R : Type u<VAR>CommSemiring R<VAR>p : ℕ<VAR>ExpChar R p<VAR>NoZeroDivisors R<VAR>f : R[X]<VAR>hf : Polynomial.derivative f = 0<GOAL>(Polynomial.expand R p) (Polynomial.contract p f) = f
<VAR>R : Type u<VAR>CommSemiring R<VAR>p : ℕ<VAR>ExpChar R p<VAR>f : R[X]<GOAL>Polynomial.map (frobenius R p) ((Polynomial.expand R p) f) = f ^ p
<VAR>R : Type u<VAR>CommSemiring R<VAR>p : ℕ<VAR>ExpChar R p<VAR>f : R[X]<VAR>n : ℕ<GOAL>Polynomial.map (frobenius R p ^ n) ((Polynomial.expand R (p ^ n)) f) = f ^ p ^ n
<VAR>R : Type u<VAR>CommRing R<VAR>p n : ℕ<VAR>ExpChar R p<VAR>f : R[X]<VAR>r : R<GOAL>Polynomial.rootMultiplicity r ((Polynomial.expand R (p ^ n)) f) = p ^ n * Polynomial.rootMultiplicity (r ^ p ^ n) f
<VAR>R : Type u<VAR>CommRing R<VAR>p : ℕ<VAR>ExpChar R p<VAR>f : R[X]<VAR>r : R<GOAL>Polynomial.rootMultiplicity r ((Polynomial.expand R p) f) = p * Polynomial.rootMultiplicity (r ^ p) f
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>p : ℕ<VAR>hp : 0 < p<GOAL>IsLocalRingHom ↑(Polynomial.expand R p)
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>p : ℕ<VAR>hp : p ≠ 0<VAR>f : R[X]<VAR>hf : Irreducible ((Polynomial.expand R p) f)<GOAL>Irreducible f
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>p : ℕ<VAR>hp : p ≠ 0<VAR>f : R[X]<VAR>n : ℕ<GOAL>Irreducible ((Polynomial.expand R (p ^ n)) f) → Irreducible f
<VAR>α : Type u_3<VAR>self : LinearOrderedAddCommMonoidWithTop α<VAR>x : α<GOAL>⊤ + x = ⊤
<VAR>α : Type u_3<VAR>self : LinearOrderedAddCommGroupWithTop α<GOAL>-⊤ = ⊤
<VAR>α : Type u_3<VAR>self : LinearOrderedAddCommGroupWithTop α<VAR>a : α<GOAL>a ≠ ⊤ → a + -a = 0
<VAR>α : Type u_1<VAR>LinearOrderedAddCommMonoidWithTop α<VAR>a : α<GOAL>⊤ + a = ⊤
<VAR>α : Type u_1<VAR>LinearOrderedAddCommMonoidWithTop α<VAR>a : α<GOAL>a + ⊤ = ⊤
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a : α<GOAL>↑(-a) = -↑a
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<GOAL>-⊤ = ⊤
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a b : α<GOAL>↑(a - b) = ↑a - ↑b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a : WithTop α<GOAL>⊤ - a = ⊤
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a : WithTop α<GOAL>a - ⊤ = ⊤
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a b : WithTop α<GOAL>a - b = ⊤ ↔ a = ⊤ ∨ b = ⊤
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>Preorder α<VAR>Preorder β<VAR>AddZeroClass α<VAR>AddZeroClass β<VAR>self : α →+o β<GOAL>Monotone (↑self.toAddMonoidHom).toFun
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>Preorder α<VAR>Preorder β<VAR>MulOneClass α<VAR>MulOneClass β<VAR>self : α →*o β<GOAL>Monotone (↑self.toMonoidHom).toFun
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>Preorder α<VAR>Preorder β<VAR>MulZeroOneClass α<VAR>MulZeroOneClass β<VAR>self : α →*₀o β<GOAL>Monotone (↑self.toMonoidWithZeroHom).toFun
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>FunLike F α β<VAR>Preorder α<VAR>Zero α<VAR>Preorder β<VAR>Zero β<VAR>OrderHomClass F α β<VAR>ZeroHomClass F α β<VAR>f : F<VAR>a : α<VAR>ha : 0 ≤ a<GOAL>0 ≤ f a
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>FunLike F α β<VAR>Preorder α<VAR>Zero α<VAR>Preorder β<VAR>Zero β<VAR>OrderHomClass F α β<VAR>ZeroHomClass F α β<VAR>f : F<VAR>a : α<VAR>ha : a ≤ 0<GOAL>f a ≤ 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommGroup α<VAR>OrderedAddCommMonoid β<VAR>i : FunLike F α β<VAR>f : F<VAR>iamhc : AddMonoidHomClass F α β<GOAL>Monotone ⇑f ↔ ∀ (a : α), 0 ≤ a → 0 ≤ f a
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommGroup α<VAR>OrderedAddCommMonoid β<VAR>i : FunLike F α β<VAR>f : F<VAR>iamhc : AddMonoidHomClass F α β<GOAL>Antitone ⇑f ↔ ∀ (a : α), 0 ≤ a → f a ≤ 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommGroup α<VAR>OrderedAddCommMonoid β<VAR>i : FunLike F α β<VAR>f : F<VAR>iamhc : AddMonoidHomClass F α β<GOAL>Monotone ⇑f ↔ ∀ (a : α), a ≤ 0 → f a ≤ 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommGroup α<VAR>OrderedAddCommMonoid β<VAR>i : FunLike F α β<VAR>f : F<VAR>iamhc : AddMonoidHomClass F α β<GOAL>Antitone ⇑f ↔ ∀ (a : α), a ≤ 0 → 0 ≤ f a
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommGroup α<VAR>OrderedAddCommMonoid β<VAR>i : FunLike F α β<VAR>f : F<VAR>CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>iamhc : AddMonoidHomClass F α β<GOAL>StrictMono ⇑f ↔ ∀ (a : α), 0 < a → 0 < f a
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommGroup α<VAR>OrderedAddCommMonoid β<VAR>i : FunLike F α β<VAR>f : F<VAR>iamhc : AddMonoidHomClass F α β<VAR>CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x < x_1<GOAL>StrictAnti ⇑f ↔ ∀ (a : α), 0 < a → f a < 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommGroup α<VAR>OrderedAddCommMonoid β<VAR>i : FunLike F α β<VAR>f : F<VAR>iamhc : AddMonoidHomClass F α β<VAR>CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x < x_1<GOAL>StrictMono ⇑f ↔ ∀ (a : α), a < 0 → f a < 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommGroup α<VAR>OrderedAddCommMonoid β<VAR>i : FunLike F α β<VAR>f : F<VAR>iamhc : AddMonoidHomClass F α β<VAR>CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x < x_1<GOAL>StrictAnti ⇑f ↔ ∀ (a : α), a < 0 → 0 < f a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>AddZeroClass α<VAR>AddZeroClass β<VAR>f g : α →+o β<VAR>h : ∀ (a : α), f a = g a<GOAL>f = g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>MulOneClass α<VAR>MulOneClass β<VAR>f g : α →*o β<VAR>h : ∀ (a : α), f a = g a<GOAL>f = g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>AddZeroClass α<VAR>AddZeroClass β<VAR>f : α →+o β<GOAL>(↑f.toAddMonoidHom).toFun = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>MulOneClass α<VAR>MulOneClass β<VAR>f : α →*o β<GOAL>(↑f.toMonoidHom).toFun = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>AddZeroClass α<VAR>AddZeroClass β<VAR>f : α →+ β<VAR>h : Monotone (↑f).toFun<GOAL>⇑{ toAddMonoidHom := f, monotone' := h } = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>MulOneClass α<VAR>MulOneClass β<VAR>f : α →* β<VAR>h : Monotone (↑f).toFun<GOAL>⇑{ toMonoidHom := f, monotone' := h } = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>AddZeroClass α<VAR>AddZeroClass β<VAR>f : α →+o β<VAR>h : Monotone (↑↑f).toFun<GOAL>{ toAddMonoidHom := ↑f, monotone' := h } = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>MulOneClass α<VAR>MulOneClass β<VAR>f : α →*o β<VAR>h : Monotone (↑↑f).toFun<GOAL>{ toMonoidHom := ↑f, monotone' := h } = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>AddZeroClass α<VAR>AddZeroClass β<VAR>f : α →+o β<GOAL>⇑↑f = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>MulOneClass α<VAR>MulOneClass β<VAR>f : α →*o β<GOAL>⇑↑f = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>MulOneClass α<VAR>MulOneClass β<GOAL>Function.Injective OrderMonoidHom.toMonoidHom
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>AddZeroClass α<VAR>AddZeroClass β<GOAL>Function.Injective OrderAddMonoidHom.toAddMonoidHom
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>MulOneClass α<VAR>MulOneClass β<GOAL>Function.Injective OrderMonoidHom.toOrderHom
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>AddZeroClass α<VAR>AddZeroClass β<GOAL>Function.Injective OrderAddMonoidHom.toOrderHom
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>MulOneClass α<VAR>MulOneClass β<VAR>f : α →*o β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>⇑(f.copy f' h) = f'
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>AddZeroClass α<VAR>AddZeroClass β<VAR>f : α →+o β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>⇑(f.copy f' h) = f'
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>MulOneClass α<VAR>MulOneClass β<VAR>f : α →*o β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>f.copy f' h = f