ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>Preorder α<VAR>AddZeroClass α<GOAL>⇑(OrderAddMonoidHom.id α) = id
<VAR>α : Type u_2<VAR>Preorder α<VAR>MulOneClass α<GOAL>⇑(OrderMonoidHom.id α) = id
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>MulOneClass α<VAR>MulOneClass β<VAR>MulOneClass γ<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>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>AddZeroClass α<VAR>AddZeroClass β<VAR>AddZeroClass γ<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>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>AddZeroClass α<VAR>AddZeroClass β<VAR>AddZeroClass γ<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>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>MulOneClass α<VAR>MulOneClass β<VAR>MulOneClass γ<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>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>AddZeroClass α<VAR>AddZeroClass β<VAR>AddZeroClass γ<VAR>f : β →+o γ<VAR>g : α →+o β<GOAL>↑(f.comp g) = (↑f).comp ↑g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>MulOneClass α<VAR>MulOneClass β<VAR>MulOneClass γ<VAR>f : β →*o γ<VAR>g : α →*o β<GOAL>↑(f.comp g) = (↑f).comp ↑g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>Preorder δ<VAR>MulOneClass α<VAR>MulOneClass β<VAR>MulOneClass γ<VAR>MulOneClass δ<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>γ : Type u_4<VAR>δ : Type u_5<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>Preorder δ<VAR>AddZeroClass α<VAR>AddZeroClass β<VAR>AddZeroClass γ<VAR>AddZeroClass δ<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>Preorder α<VAR>Preorder β<VAR>AddZeroClass α<VAR>AddZeroClass β<VAR>f : α →+o β<GOAL>f.comp (OrderAddMonoidHom.id α) = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>MulOneClass α<VAR>MulOneClass β<VAR>f : α →*o β<GOAL>f.comp (OrderMonoidHom.id α) = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>AddZeroClass α<VAR>AddZeroClass β<VAR>f : α →+o β<GOAL>(OrderAddMonoidHom.id β).comp f = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>MulOneClass α<VAR>MulOneClass β<VAR>f : α →*o β<GOAL>(OrderMonoidHom.id β).comp f = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>MulOneClass α<VAR>MulOneClass β<VAR>MulOneClass γ<VAR>g₁ g₂ : β →*o γ<VAR>f : α →*o β<VAR>hf : Function.Surjective ⇑f<GOAL>g₁.comp f = g₂.comp f ↔ g₁ = g₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>AddZeroClass α<VAR>AddZeroClass β<VAR>AddZeroClass γ<VAR>g₁ g₂ : β →+o γ<VAR>f : α →+o β<VAR>hf : Function.Surjective ⇑f<GOAL>g₁.comp f = g₂.comp f ↔ g₁ = g₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>MulOneClass α<VAR>MulOneClass β<VAR>MulOneClass γ<VAR>g : β →*o γ<VAR>f₁ f₂ : α →*o β<VAR>hg : Function.Injective ⇑g<GOAL>g.comp f₁ = g.comp f₂ ↔ f₁ = f₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>AddZeroClass α<VAR>AddZeroClass β<VAR>AddZeroClass γ<VAR>g : β →+o γ<VAR>f₁ f₂ : α →+o β<VAR>hg : Function.Injective ⇑g<GOAL>g.comp f₁ = g.comp f₂ ↔ f₁ = f₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>MulOneClass α<VAR>MulOneClass β<GOAL>⇑1 = 1
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>AddZeroClass α<VAR>AddZeroClass β<GOAL>⇑0 = 0
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>MulOneClass α<VAR>MulOneClass β<VAR>a : α<GOAL>1 a = 1
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>AddZeroClass α<VAR>AddZeroClass β<VAR>a : α<GOAL>0 a = 0
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>MulOneClass α<VAR>MulOneClass β<VAR>MulOneClass γ<VAR>f : α →*o β<GOAL>OrderMonoidHom.comp 1 f = 1
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>AddZeroClass α<VAR>AddZeroClass β<VAR>AddZeroClass γ<VAR>f : α →+o β<GOAL>OrderAddMonoidHom.comp 0 f = 0
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>AddZeroClass α<VAR>AddZeroClass β<VAR>AddZeroClass γ<VAR>f : β →+o γ<GOAL>f.comp 0 = 0
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>MulOneClass α<VAR>MulOneClass β<VAR>MulOneClass γ<VAR>f : β →*o γ<GOAL>f.comp 1 = 1
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedCommMonoid α<VAR>OrderedCommMonoid β<VAR>f g : α →*o β<GOAL>⇑(f * g) = ⇑f * ⇑g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommMonoid α<VAR>OrderedAddCommMonoid β<VAR>f g : α →+o β<GOAL>⇑(f + g) = ⇑f + ⇑g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedCommMonoid α<VAR>OrderedCommMonoid β<VAR>f g : α →*o β<VAR>a : α<GOAL>(f * g) a = f a * g a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommMonoid α<VAR>OrderedAddCommMonoid β<VAR>f g : α →+o β<VAR>a : α<GOAL>(f + g) a = f a + g a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>OrderedAddCommMonoid α<VAR>OrderedAddCommMonoid β<VAR>OrderedAddCommMonoid γ<VAR>g₁ g₂ : β →+o γ<VAR>f : α →+o β<GOAL>(g₁ + g₂).comp f = g₁.comp f + g₂.comp f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>OrderedCommMonoid α<VAR>OrderedCommMonoid β<VAR>OrderedCommMonoid γ<VAR>g₁ g₂ : β →*o γ<VAR>f : α →*o β<GOAL>(g₁ * g₂).comp f = g₁.comp f * g₂.comp f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>OrderedAddCommMonoid α<VAR>OrderedAddCommMonoid β<VAR>OrderedAddCommMonoid γ<VAR>g : β →+o γ<VAR>f₁ f₂ : α →+o β<GOAL>g.comp (f₁ + f₂) = g.comp f₁ + g.comp f₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>OrderedCommMonoid α<VAR>OrderedCommMonoid β<VAR>OrderedCommMonoid γ<VAR>g : β →*o γ<VAR>f₁ f₂ : α →*o β<GOAL>g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>hα : OrderedCommMonoid α<VAR>hβ : OrderedCommMonoid β<VAR>f : α →*o β<GOAL>f.toMonoidHom = ↑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>hα : OrderedAddCommMonoid α<VAR>hβ : OrderedAddCommMonoid β<VAR>f : α →+o β<GOAL>f.toAddMonoidHom = ↑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>hα : OrderedAddCommMonoid α<VAR>hβ : OrderedAddCommMonoid β<VAR>f : α →+o β<GOAL>f.toOrderHom = ↑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>hα : OrderedCommMonoid α<VAR>hβ : OrderedCommMonoid β<VAR>f : α →*o β<GOAL>f.toOrderHom = ↑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>MulZeroOneClass α<VAR>MulZeroOneClass β<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>MulZeroOneClass α<VAR>MulZeroOneClass β<VAR>f : α →*₀o β<GOAL>(↑f.toMonoidWithZeroHom).toFun = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>MulZeroOneClass α<VAR>MulZeroOneClass β<VAR>f : α →*₀ β<VAR>h : Monotone (↑f).toFun<GOAL>⇑{ toMonoidWithZeroHom := f, monotone' := h } = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>MulZeroOneClass α<VAR>MulZeroOneClass β<VAR>f : α →*₀o β<VAR>h : Monotone (↑↑f).toFun<GOAL>{ toMonoidWithZeroHom := ↑f, monotone' := h } = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>MulZeroOneClass α<VAR>MulZeroOneClass β<VAR>f : α →*₀o β<GOAL>⇑↑f = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>MulZeroOneClass α<VAR>MulZeroOneClass β<GOAL>Function.Injective OrderMonoidWithZeroHom.toOrderMonoidHom
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>MulZeroOneClass α<VAR>MulZeroOneClass β<GOAL>Function.Injective OrderMonoidWithZeroHom.toMonoidWithZeroHom
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>MulZeroOneClass α<VAR>MulZeroOneClass β<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>MulZeroOneClass α<VAR>MulZeroOneClass β<VAR>f : α →*₀o β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>f.copy f' h = ↑f
<VAR>α : Type u_2<VAR>Preorder α<VAR>MulZeroOneClass α<GOAL>⇑(OrderMonoidWithZeroHom.id α) = id
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>MulZeroOneClass α<VAR>MulZeroOneClass β<VAR>MulZeroOneClass γ<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>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>MulZeroOneClass α<VAR>MulZeroOneClass β<VAR>MulZeroOneClass γ<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>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>MulZeroOneClass α<VAR>MulZeroOneClass β<VAR>MulZeroOneClass γ<VAR>f : β →*₀o γ<VAR>g : α →*₀o β<GOAL>↑(f.comp g) = (↑f).comp ↑g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>Preorder δ<VAR>MulZeroOneClass α<VAR>MulZeroOneClass β<VAR>MulZeroOneClass γ<VAR>MulZeroOneClass δ<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>Preorder α<VAR>Preorder β<VAR>MulZeroOneClass α<VAR>MulZeroOneClass β<VAR>f : α →*₀o β<GOAL>f.comp (OrderMonoidWithZeroHom.id α) = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>MulZeroOneClass α<VAR>MulZeroOneClass β<VAR>f : α →*₀o β<GOAL>(OrderMonoidWithZeroHom.id β).comp f = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>MulZeroOneClass α<VAR>MulZeroOneClass β<VAR>MulZeroOneClass γ<VAR>g₁ g₂ : β →*₀o γ<VAR>f : α →*₀o β<VAR>hf : Function.Surjective ⇑f<GOAL>g₁.comp f = g₂.comp f ↔ g₁ = g₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>MulZeroOneClass α<VAR>MulZeroOneClass β<VAR>MulZeroOneClass γ<VAR>g : β →*₀o γ<VAR>f₁ f₂ : α →*₀o β<VAR>hg : Function.Injective ⇑g<GOAL>g.comp f₁ = g.comp f₂ ↔ f₁ = f₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedCommMonoidWithZero α<VAR>LinearOrderedCommMonoidWithZero β<VAR>f g : α →*₀o β<GOAL>⇑(f * g) = ⇑f * ⇑g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedCommMonoidWithZero α<VAR>LinearOrderedCommMonoidWithZero β<VAR>f g : α →*₀o β<VAR>a : α<GOAL>(f * g) a = f a * g a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>LinearOrderedCommMonoidWithZero α<VAR>LinearOrderedCommMonoidWithZero β<VAR>LinearOrderedCommMonoidWithZero γ<VAR>g₁ g₂ : β →*₀o γ<VAR>f : α →*₀o β<GOAL>(g₁ * g₂).comp f = g₁.comp f * g₂.comp f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>LinearOrderedCommMonoidWithZero α<VAR>LinearOrderedCommMonoidWithZero β<VAR>LinearOrderedCommMonoidWithZero γ<VAR>g : β →*₀o γ<VAR>f₁ f₂ : α →*₀o β<GOAL>g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>hα : Preorder α<VAR>hα' : MulZeroOneClass α<VAR>hβ : Preorder β<VAR>hβ' : MulZeroOneClass β<VAR>f : α →*₀o β<GOAL>f.toMonoidWithZeroHom = ↑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>hα : Preorder α<VAR>hα' : MulZeroOneClass α<VAR>hβ : Preorder β<VAR>hβ' : MulZeroOneClass β<VAR>f : α →*₀o β<GOAL>f.toOrderMonoidHom = ↑f
<VAR>R : Type u_1<VAR>Semiring R<VAR>p q : R[T;T⁻¹]<VAR>h : ∀ (a : ℤ), p a = q a<GOAL>p = q
<VAR>R : Type u_1<VAR>Semiring R<VAR>p : R[X]<GOAL>Polynomial.toLaurent p = AddMonoidAlgebra.mapDomain Nat.cast p.toFinsupp
<VAR>R : Type u_1<VAR>CommSemiring R<GOAL>⇑Polynomial.toLaurentAlg = ⇑Polynomial.toLaurent
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>f : R[X]<GOAL>Polynomial.toLaurentAlg f = Polynomial.toLaurent f
<VAR>R : Type u_1<VAR>Semiring R<GOAL>Finsupp.single 0 1 = 1
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>r : R<GOAL>(algebraMap R A[T;T⁻¹]) r = LaurentPolynomial.C ((algebraMap R A) r)
<VAR>R : Type u_2<VAR>CommSemiring R<VAR>r : R<GOAL>LaurentPolynomial.C r = (algebraMap R R[T;T⁻¹]) r
<VAR>R : Type u_1<VAR>Semiring R<VAR>r : R<GOAL>Finsupp.single 0 r = LaurentPolynomial.C r
<VAR>R : Type u_1<VAR>Semiring R<VAR>t : R<VAR>n : ℤ<GOAL>(LaurentPolynomial.C t) n = if n = 0 then t else 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>m n : ℤ<GOAL>(LaurentPolynomial.T n) m = if n = m then 1 else 0
<VAR>R : Type u_1<VAR>Semiring R<GOAL>LaurentPolynomial.T 0 = 1
<VAR>R : Type u_1<VAR>Semiring R<VAR>m n : ℤ<GOAL>LaurentPolynomial.T (m + n) = LaurentPolynomial.T m * LaurentPolynomial.T n
<VAR>R : Type u_1<VAR>Semiring R<VAR>m n : ℤ<GOAL>LaurentPolynomial.T (m - n) = LaurentPolynomial.T m * LaurentPolynomial.T (-n)
<VAR>R : Type u_1<VAR>Semiring R<VAR>m : ℤ<VAR>n : ℕ<GOAL>LaurentPolynomial.T m ^ n = LaurentPolynomial.T (↑n * m)
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : R[T;T⁻¹]<VAR>m n : ℤ<GOAL>f * LaurentPolynomial.T m * LaurentPolynomial.T n = f * LaurentPolynomial.T (m + n)
<VAR>R : Type u_1<VAR>Semiring R<VAR>r : R<VAR>n : ℤ<GOAL>Finsupp.single n r = LaurentPolynomial.C r * LaurentPolynomial.T n
<VAR>R : Type u_1<VAR>Semiring R<VAR>n : ℕ<VAR>r : R<GOAL>Polynomial.toLaurent ((Polynomial.monomial n) r) = LaurentPolynomial.C r * LaurentPolynomial.T ↑n
<VAR>R : Type u_1<VAR>Semiring R<VAR>r : R<GOAL>Polynomial.toLaurent (Polynomial.C r) = LaurentPolynomial.C r
<VAR>R : Type u_1<VAR>Semiring R<GOAL>⇑Polynomial.toLaurent ∘ ⇑Polynomial.C = ⇑LaurentPolynomial.C
<VAR>R : Type u_1<VAR>Semiring R<GOAL>Polynomial.toLaurent Polynomial.X = LaurentPolynomial.T 1
<VAR>R : Type u_1<VAR>Semiring R<GOAL>Polynomial.toLaurent 1 = 1
<VAR>R : Type u_1<VAR>Semiring R<VAR>r : R<VAR>f : R[X]<GOAL>Polynomial.toLaurent (Polynomial.C r * f) = LaurentPolynomial.C r * Polynomial.toLaurent f
<VAR>R : Type u_1<VAR>Semiring R<VAR>n : ℕ<GOAL>Polynomial.toLaurent (Polynomial.X ^ n) = LaurentPolynomial.T ↑n
<VAR>R : Type u_1<VAR>Semiring R<VAR>n : ℕ<VAR>r : R<GOAL>Polynomial.toLaurent (Polynomial.C r * Polynomial.X ^ n) = LaurentPolynomial.C r * LaurentPolynomial.T ↑n
<VAR>R : Type u_1<VAR>Semiring R<VAR>n : ℤ<GOAL>⅟(LaurentPolynomial.T n) = LaurentPolynomial.T (-n)
<VAR>R : Type u_1<VAR>Semiring R<VAR>n : ℤ<GOAL>IsUnit (LaurentPolynomial.T n)
<VAR>R : Type u_1<VAR>Semiring R<VAR>M : R[T;T⁻¹] → Prop<VAR>p : R[T;T⁻¹]<VAR>h_C : ∀ (a : R), M (LaurentPolynomial.C a)<VAR>h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)<VAR>h_C_mul_T : ∀ (n : ℕ) (a : R), M (LaurentPolynomial.C a * LaurentPolynomial.T ↑n) → M (LaurentPolynomial.C a * LaurentPolynomial.T (↑n + 1))<VAR>h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (LaurentPolynomial.C a * LaurentPolynomial.T (-↑n)) → M (LaurentPolynomial.C a * LaurentPolynomial.T (-↑n - 1))<GOAL>M p
<VAR>R : Type u_1<VAR>Semiring R<VAR>M : R[T;T⁻¹] → Prop<VAR>p : R[T;T⁻¹]<VAR>h_add : ∀ (p q : R[T;T⁻¹]), M p → M q → M (p + q)<VAR>h_C_mul_T : ∀ (n : ℤ) (a : R), M (LaurentPolynomial.C a * LaurentPolynomial.T n)<GOAL>M p
<VAR>R : Type u_1<VAR>Semiring R<VAR>n : ℤ<VAR>f : R[T;T⁻¹]<GOAL>Commute (LaurentPolynomial.T n) f
<VAR>R : Type u_1<VAR>Semiring R<VAR>n : ℤ<VAR>f : R[T;T⁻¹]<GOAL>LaurentPolynomial.T n * f = f * LaurentPolynomial.T n
<VAR>R : Type u_1<VAR>Semiring R<VAR>n : ℤ<VAR>r : R<GOAL>LaurentPolynomial.trunc (LaurentPolynomial.C r * LaurentPolynomial.T n) = if 0 ≤ n then (Polynomial.monomial n.toNat) r else 0
<VAR>R : Type u_1<VAR>Semiring R<GOAL>Function.LeftInverse ⇑LaurentPolynomial.trunc ⇑Polynomial.toLaurent
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : R[X]<GOAL>LaurentPolynomial.trunc (Polynomial.toLaurent f) = f
<VAR>R : Type u_1<VAR>Semiring R<GOAL>Function.Injective ⇑Polynomial.toLaurent
<VAR>R : Type u_1<VAR>Semiring R<VAR>f g : R[X]<GOAL>Polynomial.toLaurent f = Polynomial.toLaurent g ↔ f = g
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : R[X]<GOAL>f ≠ 0 ↔ Polynomial.toLaurent f ≠ 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : R[T;T⁻¹]<GOAL>∃ n f', Polynomial.toLaurent f' = f * LaurentPolynomial.T ↑n
<VAR>R : Type u_1<VAR>Semiring R<VAR>Q : R[T;T⁻¹] → Prop<VAR>f : R[T;T⁻¹]<VAR>Qf : ∀ {f : R[X]} {n : ℕ}, Q (Polynomial.toLaurent f * LaurentPolynomial.T (-↑n))<GOAL>Q f
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : R[T;T⁻¹]<VAR>Q : R[T;T⁻¹] → Prop<VAR>Qf : ∀ (f : R[X]), Q (Polynomial.toLaurent f)<VAR>QT : ∀ (f : R[T;T⁻¹]), Q (f * LaurentPolynomial.T 1) → Q f<GOAL>Q f
<VAR>R : Type u_1<VAR>Semiring R<VAR>a : R<VAR>n : ℤ<GOAL>(LaurentPolynomial.C a * LaurentPolynomial.T n).support ⊆ {n}
<VAR>R : Type u_1<VAR>Semiring R<VAR>a : R<VAR>a0 : a ≠ 0<VAR>n : ℤ<GOAL>(LaurentPolynomial.C a * LaurentPolynomial.T n).support = {n}
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : R[X]<GOAL>(Polynomial.toLaurent f).support = Finset.map Nat.castEmbedding f.support
<VAR>R : Type u_1<VAR>Semiring R<GOAL>LaurentPolynomial.degree 0 = ⊥
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : R[T;T⁻¹]<GOAL>f.degree = ⊥ ↔ f = 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>n : ℤ<VAR>a : R<VAR>a0 : a ≠ 0<GOAL>(LaurentPolynomial.C a * LaurentPolynomial.T n).degree = ↑n
<VAR>R : Type u_1<VAR>Semiring R<VAR>DecidableEq R<VAR>n : ℤ<VAR>a : R<GOAL>(LaurentPolynomial.C a * LaurentPolynomial.T n).degree = if a = 0 then ⊥ else ↑n
<VAR>R : Type u_1<VAR>Semiring R<VAR>Nontrivial R<VAR>n : ℤ<GOAL>(LaurentPolynomial.T n).degree = ↑n
<VAR>R : Type u_1<VAR>Semiring R<VAR>a : R<VAR>a0 : a ≠ 0<GOAL>(LaurentPolynomial.C a).degree = 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>DecidableEq R<VAR>a : R<GOAL>(LaurentPolynomial.C a).degree = if a = 0 then ⊥ else 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>n : ℤ<VAR>a : R<GOAL>(LaurentPolynomial.C a * LaurentPolynomial.T n).degree ≤ ↑n
<VAR>R : Type u_1<VAR>Semiring R<VAR>n : ℤ<GOAL>(LaurentPolynomial.T n).degree ≤ ↑n
<VAR>R : Type u_1<VAR>Semiring R<VAR>a : R<GOAL>(LaurentPolynomial.C a).degree ≤ 0
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>n : ℕ<GOAL>(algebraMap R[X] R[T;T⁻¹]) (Polynomial.X ^ n) = LaurentPolynomial.T ↑n
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>f : R[X]<GOAL>(algebraMap R[X] R[T;T⁻¹]) f = Polynomial.toLaurent f
<VAR>R : Type u_1<VAR>CommSemiring R<GOAL>IsLocalization (Submonoid.closure {Polynomial.X}) R[T;T⁻¹]
<VAR>R : Type u_2<VAR>CommSemiring R<VAR>n : ℤ<GOAL>LaurentPolynomial.invert (LaurentPolynomial.T n) = LaurentPolynomial.T (-n)
<VAR>R : Type u_2<VAR>CommSemiring R<VAR>f : R[T;T⁻¹]<VAR>n : ℤ<GOAL>(LaurentPolynomial.invert f) n = f (-n)
<VAR>R : Type u_2<VAR>CommSemiring R<GOAL>⇑LaurentPolynomial.invert ∘ ⇑LaurentPolynomial.C = ⇑LaurentPolynomial.C
<VAR>R : Type u_2<VAR>CommSemiring R<VAR>t : R<GOAL>LaurentPolynomial.invert (LaurentPolynomial.C t) = LaurentPolynomial.C t
<VAR>R : Type u_2<VAR>CommSemiring R<GOAL>Function.Involutive ⇑LaurentPolynomial.invert
<VAR>R : Type u_2<VAR>CommSemiring R<GOAL>LaurentPolynomial.invert.symm = LaurentPolynomial.invert
<VAR>R : Type u_2<VAR>CommSemiring R<VAR>p : R[X]<GOAL>Polynomial.toLaurent p.reverse = LaurentPolynomial.invert (Polynomial.toLaurent p) * LaurentPolynomial.T ↑p.natDegree
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>i : ℕ<GOAL>0 i = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>g₁ g₂ : PolynomialModule R M<VAR>a : ℕ<GOAL>(g₁ + g₂) a = g₁ a + g₂ a
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>i : ℕ<VAR>m : M<VAR>n : ℕ<GOAL>((PolynomialModule.single R i) m) n = if i = n then m else 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>i : ℕ<VAR>m : M<VAR>n : ℕ<GOAL>((PolynomialModule.lsingle R i) m) n = if i = n then m else 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>i : ℕ<VAR>r : R<VAR>m : M<GOAL>(PolynomialModule.single R i) (r • m) = r • (PolynomialModule.single R i) m
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>P : PolynomialModule R M → Prop<VAR>f : PolynomialModule R M<VAR>h0 : P 0<VAR>hadd : ∀ (f g : PolynomialModule R M), P f → P g → P (f + g)<VAR>hsingle : ∀ (a : ℕ) (b : M), P ((PolynomialModule.single R a) b)<GOAL>P f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>f : R[X]<VAR>m : PolynomialModule R M<GOAL>f • m = ((Polynomial.aeval (Finsupp.lmapDomain M R Nat.succ)) f) m
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>i : ℕ<VAR>r : R<VAR>j : ℕ<VAR>m : M<GOAL>(Polynomial.monomial i) r • (PolynomialModule.single R j) m = (PolynomialModule.single R (i + j)) (r • m)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>i : ℕ<VAR>r : R<VAR>g : PolynomialModule R M<VAR>n : ℕ<GOAL>((Polynomial.monomial i) r • g) n = if i ≤ n then r • g (n - i) else 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>i : ℕ<VAR>f : R[X]<VAR>m : M<VAR>n : ℕ<GOAL>(f • (PolynomialModule.single R i) m) n = if i ≤ n then f.coeff (n - i) • m else 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>f : R[X]<VAR>g : PolynomialModule R M<VAR>n : ℕ<GOAL>(f • g) n = ∑ x ∈ Finset.antidiagonal n, f.coeff x.1 • g x.2
<VAR>R : Type u_1<VAR>CommRing R<VAR>p : PolynomialModule R R<GOAL>PolynomialModule.equivPolynomialSelf p = PolynomialModule.equivPolynomial p
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_4<VAR>CommRing S<VAR>Algebra R S<VAR>n : ℕ<VAR>x : S<GOAL>PolynomialModule.equivPolynomial ((PolynomialModule.single R n) x) = (Polynomial.monomial n) x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>R' : Type u_4<VAR>M' : Type u_5<VAR>CommRing R'<VAR>AddCommGroup M'<VAR>Module R' M'<VAR>Module R M'<VAR>f : M →ₗ[R] M'<VAR>i : ℕ<VAR>m : M<GOAL>(PolynomialModule.map R' f) ((PolynomialModule.single R i) m) = (PolynomialModule.single R' i) (f m)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>R' : Type u_4<VAR>M' : Type u_5<VAR>CommRing R'<VAR>AddCommGroup M'<VAR>Module R' M'<VAR>Algebra R R'<VAR>Module R M'<VAR>IsScalarTower R R' M'<VAR>f : M →ₗ[R] M'<VAR>p : R[X]<VAR>q : PolynomialModule R M<GOAL>(PolynomialModule.map R' f) (p • q) = Polynomial.map (algebraMap R R') p • (PolynomialModule.map R' f) q
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>r : R<VAR>p : PolynomialModule R M<GOAL>(PolynomialModule.eval r) p = Finsupp.sum p fun i m => r ^ i • m
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>r : R<VAR>i : ℕ<VAR>m : M<GOAL>(PolynomialModule.eval r) ((PolynomialModule.single R i) m) = r ^ i • m
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>r : R<VAR>i : ℕ<VAR>m : M<GOAL>(PolynomialModule.eval r) ((PolynomialModule.lsingle R i) m) = r ^ i • m
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : R[X]<VAR>q : PolynomialModule R M<VAR>r : R<GOAL>(PolynomialModule.eval r) (p • q) = Polynomial.eval r p • (PolynomialModule.eval r) q
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>R' : Type u_4<VAR>M' : Type u_5<VAR>CommRing R'<VAR>AddCommGroup M'<VAR>Module R' M'<VAR>Algebra R R'<VAR>Module R M'<VAR>IsScalarTower R R' M'<VAR>f : M →ₗ[R] M'<VAR>q : PolynomialModule R M<VAR>r : R<GOAL>(PolynomialModule.eval ((algebraMap R R') r)) ((PolynomialModule.map R' f) q) = f ((PolynomialModule.eval r) q)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>f : M →ₗ[R] M<VAR>q : PolynomialModule R M<VAR>r : R<GOAL>(PolynomialModule.eval r) ((PolynomialModule.map R f) q) = f ((PolynomialModule.eval r) q)
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_6<VAR>CommRing S<VAR>Algebra S R<VAR>f : PolynomialModule S S<VAR>x : R<GOAL>(Polynomial.aeval x) (PolynomialModule.equivPolynomial f) = (PolynomialModule.eval x) ((PolynomialModule.map R (Algebra.linearMap S R)) f)