ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>S : Type u_7<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>module_M : Module R M<VAR>module_S_M₂ : Module S M₂<VAR>σ : R →+* S<VAR>σ' : S →+* R<VAR>re₁ : RingHomInvPair σ σ'<VAR>re₂ : RingHomInvPair σ' σ<VAR>e : M ≃ₛₗ[σ] M₂<GOAL>Function.Surjective ⇑e
<VAR>R : Type u_1<VAR>S : Type u_7<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>module_M : Module R M<VAR>module_S_M₂ : Module S M₂<VAR>σ : R →+* S<VAR>σ' : S →+* R<VAR>re₁ : RingHomInvPair σ σ'<VAR>re₂ : RingHomInvPair σ' σ<VAR>e : M ≃ₛₗ[σ] M₂<VAR>s : Set M<GOAL>⇑e '' s = ⇑e.symm ⁻¹' s
<VAR>R : Type u_1<VAR>S : Type u_7<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>module_M : Module R M<VAR>module_S_M₂ : Module S M₂<VAR>σ : R →+* S<VAR>σ' : S →+* R<VAR>re₁ : RingHomInvPair σ σ'<VAR>re₂ : RingHomInvPair σ' σ<VAR>e : M ≃ₛₗ[σ] M₂<VAR>s : Set M₂<GOAL>⇑e.symm '' s = ⇑e ⁻¹' s
<VAR>R : Type u_1<VAR>S : Type u_7<VAR>Semiring R<VAR>Semiring S<VAR>f : R ≃+* S<VAR>a : R<GOAL>f.toSemilinearEquiv a = f a
<VAR>R : Type u_1<VAR>S : Type u_7<VAR>Semiring R<VAR>Semiring S<VAR>f : R ≃+* S<GOAL>∀ (a : S), f.toSemilinearEquiv.symm a = f.invFun a
<VAR>R : Type u_1<VAR>M : Type u_8<VAR>Semiring R<VAR>AddCommMonoid M<VAR>σ σ' : R →+* R<VAR>RingHomInvPair σ σ'<VAR>RingHomInvPair σ' σ<GOAL>∀ {x : Module R M} (f : M →ₛₗ[σ] M) (hf : Function.Involutive ⇑f), ⇑(LinearEquiv.ofInvolutive f hf) = ⇑f
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<VAR>p : ℕ<VAR>r : R<GOAL>(MvPolynomial.expand p) (MvPolynomial.C r) = MvPolynomial.C r
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<VAR>p : ℕ<VAR>i : σ<GOAL>(MvPolynomial.expand p) (MvPolynomial.X i) = MvPolynomial.X i ^ p
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<VAR>p : ℕ<VAR>d : σ →₀ ℕ<VAR>r : R<GOAL>(MvPolynomial.expand p) ((MvPolynomial.monomial d) r) = MvPolynomial.C r * ∏ i ∈ d.support, (MvPolynomial.X i ^ p) ^ d i
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<VAR>f : MvPolynomial σ R<GOAL>(MvPolynomial.expand 1) f = f
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<GOAL>MvPolynomial.expand 1 = AlgHom.id R (MvPolynomial σ R)
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>CommSemiring R<VAR>p : ℕ<VAR>f : σ → MvPolynomial τ R<GOAL>(MvPolynomial.expand p).comp (MvPolynomial.bind₁ f) = MvPolynomial.bind₁ fun i => (MvPolynomial.expand p) (f i)
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>CommSemiring R<VAR>p : ℕ<VAR>f : σ → MvPolynomial τ R<VAR>φ : MvPolynomial σ R<GOAL>(MvPolynomial.expand p) ((MvPolynomial.bind₁ f) φ) = (MvPolynomial.bind₁ fun i => (MvPolynomial.expand p) (f i)) φ
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>S : Type u_4<VAR>CommSemiring R<VAR>CommSemiring S<VAR>f : R →+* S<VAR>p : ℕ<VAR>φ : MvPolynomial σ R<GOAL>(MvPolynomial.map f) ((MvPolynomial.expand p) φ) = (MvPolynomial.expand p) ((MvPolynomial.map f) φ)
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>CommSemiring R<VAR>f : σ → τ<VAR>p : ℕ<VAR>φ : MvPolynomial σ R<GOAL>(MvPolynomial.rename f) ((MvPolynomial.expand p) φ) = (MvPolynomial.expand p) ((MvPolynomial.rename f) φ)
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>CommSemiring R<VAR>f : σ → τ<VAR>p : ℕ<GOAL>(MvPolynomial.rename f).comp (MvPolynomial.expand p) = (MvPolynomial.expand p).comp (MvPolynomial.rename f)
<VAR>α : Type u_1<GOAL>FreeMonoid.toList.symm = FreeMonoid.ofList
<VAR>α : Type u_1<GOAL>FreeAddMonoid.toList.symm = FreeAddMonoid.ofList
<VAR>α : Type u_1<GOAL>FreeMonoid.ofList.symm = FreeMonoid.toList
<VAR>α : Type u_1<GOAL>FreeAddMonoid.ofList.symm = FreeAddMonoid.toList
<VAR>α : Type u_1<VAR>l : List α<GOAL>FreeAddMonoid.toList (FreeAddMonoid.ofList l) = l
<VAR>α : Type u_1<VAR>l : List α<GOAL>FreeMonoid.toList (FreeMonoid.ofList l) = l
<VAR>α : Type u_1<VAR>xs : FreeAddMonoid α<GOAL>FreeAddMonoid.ofList (FreeAddMonoid.toList xs) = xs
<VAR>α : Type u_1<VAR>xs : FreeMonoid α<GOAL>FreeMonoid.ofList (FreeMonoid.toList xs) = xs
<VAR>α : Type u_1<GOAL>⇑FreeMonoid.toList ∘ ⇑FreeMonoid.ofList = id
<VAR>α : Type u_1<GOAL>⇑FreeAddMonoid.toList ∘ ⇑FreeAddMonoid.ofList = id
<VAR>α : Type u_1<GOAL>⇑FreeAddMonoid.ofList ∘ ⇑FreeAddMonoid.toList = id
<VAR>α : Type u_1<GOAL>⇑FreeMonoid.ofList ∘ ⇑FreeMonoid.toList = id
<VAR>α : Type u_1<GOAL>FreeAddMonoid.toList 0 = []
<VAR>α : Type u_1<GOAL>FreeMonoid.toList 1 = []
<VAR>α : Type u_1<GOAL>FreeAddMonoid.ofList [] = 0
<VAR>α : Type u_1<GOAL>FreeMonoid.ofList [] = 1
<VAR>α : Type u_1<VAR>xs ys : FreeMonoid α<GOAL>FreeMonoid.toList (xs * ys) = FreeMonoid.toList xs ++ FreeMonoid.toList ys
<VAR>α : Type u_1<VAR>xs ys : FreeAddMonoid α<GOAL>FreeAddMonoid.toList (xs + ys) = FreeAddMonoid.toList xs ++ FreeAddMonoid.toList ys
<VAR>α : Type u_1<VAR>xs ys : List α<GOAL>FreeMonoid.ofList (xs ++ ys) = FreeMonoid.ofList xs * FreeMonoid.ofList ys
<VAR>α : Type u_1<VAR>xs ys : List α<GOAL>FreeAddMonoid.ofList (xs ++ ys) = FreeAddMonoid.ofList xs + FreeAddMonoid.ofList ys
<VAR>α : Type u_1<VAR>xs : List (FreeAddMonoid α)<GOAL>FreeAddMonoid.toList xs.sum = (List.map (⇑FreeAddMonoid.toList) xs).join
<VAR>α : Type u_1<VAR>xs : List (FreeMonoid α)<GOAL>FreeMonoid.toList xs.prod = (List.map (⇑FreeMonoid.toList) xs).join
<VAR>α : Type u_1<VAR>xs : List (List α)<GOAL>FreeMonoid.ofList xs.join = (List.map (⇑FreeMonoid.ofList) xs).prod
<VAR>α : Type u_1<VAR>xs : List (List α)<GOAL>FreeAddMonoid.ofList xs.join = (List.map (⇑FreeAddMonoid.ofList) xs).sum
<VAR>α : Type u_1<VAR>x : α<GOAL>FreeMonoid.toList (FreeMonoid.of x) = [x]
<VAR>α : Type u_1<VAR>x : α<GOAL>FreeAddMonoid.toList (FreeAddMonoid.of x) = [x]
<VAR>α : Type u_1<VAR>x : α<GOAL>FreeAddMonoid.ofList [x] = FreeAddMonoid.of x
<VAR>α : Type u_1<VAR>x : α<GOAL>FreeMonoid.ofList [x] = FreeMonoid.of x
<VAR>α : Type u_1<VAR>x : α<VAR>xs : List α<GOAL>FreeMonoid.ofList (x :: xs) = FreeMonoid.of x * FreeMonoid.ofList xs
<VAR>α : Type u_1<VAR>x : α<VAR>xs : List α<GOAL>FreeAddMonoid.ofList (x :: xs) = FreeAddMonoid.of x + FreeAddMonoid.ofList xs
<VAR>α : Type u_1<VAR>x : α<VAR>xs : FreeAddMonoid α<GOAL>FreeAddMonoid.toList (FreeAddMonoid.of x + xs) = x :: FreeAddMonoid.toList xs
<VAR>α : Type u_1<VAR>x : α<VAR>xs : FreeMonoid α<GOAL>FreeMonoid.toList (FreeMonoid.of x * xs) = x :: FreeMonoid.toList xs
<VAR>α : Type u_1<GOAL>Function.Injective FreeAddMonoid.of
<VAR>α : Type u_1<GOAL>Function.Injective FreeMonoid.of
<VAR>α : Type u_1<VAR>C : FreeMonoid α → Sort u_6<VAR>h0 : C 1<VAR>ih : (x : α) → (xs : FreeMonoid α) → C xs → C (FreeMonoid.of x * xs)<GOAL>FreeMonoid.recOn 1 h0 ih = h0
<VAR>α : Type u_1<VAR>C : FreeAddMonoid α → Sort u_6<VAR>h0 : C 0<VAR>ih : (x : α) → (xs : FreeAddMonoid α) → C xs → C (FreeAddMonoid.of x + xs)<GOAL>FreeAddMonoid.recOn 0 h0 ih = h0
<VAR>α : Type u_1<VAR>C : FreeMonoid α → Sort u_6<VAR>x : α<VAR>xs : FreeMonoid α<VAR>h0 : C 1<VAR>ih : (x : α) → (xs : FreeMonoid α) → C xs → C (FreeMonoid.of x * xs)<GOAL>(FreeMonoid.of x * xs).recOn h0 ih = ih x xs (xs.recOn h0 ih)
<VAR>α : Type u_1<VAR>C : FreeAddMonoid α → Sort u_6<VAR>x : α<VAR>xs : FreeAddMonoid α<VAR>h0 : C 0<VAR>ih : (x : α) → (xs : FreeAddMonoid α) → C xs → C (FreeAddMonoid.of x + xs)<GOAL>(FreeAddMonoid.of x + xs).recOn h0 ih = ih x xs (xs.recOn h0 ih)
<VAR>α : Type u_1<VAR>C : FreeMonoid α → Sort u_6<VAR>h0 : C 1<VAR>ih : (x : α) → (xs : FreeMonoid α) → C (FreeMonoid.of x * xs)<GOAL>FreeMonoid.casesOn 1 h0 ih = h0
<VAR>α : Type u_1<VAR>C : FreeAddMonoid α → Sort u_6<VAR>h0 : C 0<VAR>ih : (x : α) → (xs : FreeAddMonoid α) → C (FreeAddMonoid.of x + xs)<GOAL>FreeAddMonoid.casesOn 0 h0 ih = h0
<VAR>α : Type u_1<VAR>C : FreeAddMonoid α → Sort u_6<VAR>x : α<VAR>xs : FreeAddMonoid α<VAR>h0 : C 0<VAR>ih : (x : α) → (xs : FreeAddMonoid α) → C (FreeAddMonoid.of x + xs)<GOAL>(FreeAddMonoid.of x + xs).casesOn h0 ih = ih x xs
<VAR>α : Type u_1<VAR>C : FreeMonoid α → Sort u_6<VAR>x : α<VAR>xs : FreeMonoid α<VAR>h0 : C 1<VAR>ih : (x : α) → (xs : FreeMonoid α) → C (FreeMonoid.of x * xs)<GOAL>(FreeMonoid.of x * xs).casesOn h0 ih = ih x xs
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>AddMonoid M<VAR>f g : FreeAddMonoid α →+ M<VAR>h : ∀ (x : α), f (FreeAddMonoid.of x) = g (FreeAddMonoid.of x)<GOAL>f = g
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>Monoid M<VAR>f g : FreeMonoid α →* M<VAR>h : ∀ (x : α), f (FreeMonoid.of x) = g (FreeMonoid.of x)<GOAL>f = g
<VAR>M : Type u_4<VAR>AddMonoid M<VAR>l : List M<GOAL>FreeAddMonoid.sumAux l = l.sum
<VAR>M : Type u_4<VAR>Monoid M<VAR>l : List M<GOAL>FreeMonoid.prodAux l = l.prod
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>Monoid M<VAR>f : α → M<VAR>l : List α<GOAL>(FreeMonoid.lift f) (FreeMonoid.ofList l) = (List.map f l).prod
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>AddMonoid M<VAR>f : α → M<VAR>l : List α<GOAL>(FreeAddMonoid.lift f) (FreeAddMonoid.ofList l) = (List.map f l).sum
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>AddMonoid M<VAR>f : FreeAddMonoid α →+ M<GOAL>FreeAddMonoid.lift.symm f = ⇑f ∘ FreeAddMonoid.of
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>Monoid M<VAR>f : FreeMonoid α →* M<GOAL>FreeMonoid.lift.symm f = ⇑f ∘ FreeMonoid.of
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>Monoid M<VAR>f : α → M<VAR>l : FreeMonoid α<GOAL>(FreeMonoid.lift f) l = (List.map f (FreeMonoid.toList l)).prod
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>AddMonoid M<VAR>f : α → M<VAR>l : FreeAddMonoid α<GOAL>(FreeAddMonoid.lift f) l = (List.map f (FreeAddMonoid.toList l)).sum
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>Monoid M<VAR>f : α → M<GOAL>⇑(FreeMonoid.lift f) ∘ FreeMonoid.of = f
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>AddMonoid M<VAR>f : α → M<GOAL>⇑(FreeAddMonoid.lift f) ∘ FreeAddMonoid.of = f
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>AddMonoid M<VAR>f : α → M<VAR>x : α<GOAL>(FreeAddMonoid.lift f) (FreeAddMonoid.of x) = f x
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>Monoid M<VAR>f : α → M<VAR>x : α<GOAL>(FreeMonoid.lift f) (FreeMonoid.of x) = f x
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>AddMonoid M<VAR>f : FreeAddMonoid α →+ M<GOAL>FreeAddMonoid.lift (⇑f ∘ FreeAddMonoid.of) = f
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>Monoid M<VAR>f : FreeMonoid α →* M<GOAL>FreeMonoid.lift (⇑f ∘ FreeMonoid.of) = f
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>AddMonoid M<VAR>N : Type u_5<VAR>AddMonoid N<VAR>g : M →+ N<VAR>f : α → M<GOAL>g.comp (FreeAddMonoid.lift f) = FreeAddMonoid.lift (⇑g ∘ f)
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>Monoid M<VAR>N : Type u_5<VAR>Monoid N<VAR>g : M →* N<VAR>f : α → M<GOAL>g.comp (FreeMonoid.lift f) = FreeMonoid.lift (⇑g ∘ f)
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>Monoid M<VAR>N : Type u_5<VAR>Monoid N<VAR>g : M →* N<VAR>f : α → M<VAR>x : FreeMonoid α<GOAL>g ((FreeMonoid.lift f) x) = (FreeMonoid.lift (⇑g ∘ f)) x
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>AddMonoid M<VAR>N : Type u_5<VAR>AddMonoid N<VAR>g : M →+ N<VAR>f : α → M<VAR>x : FreeAddMonoid α<GOAL>g ((FreeAddMonoid.lift f) x) = (FreeAddMonoid.lift (⇑g ∘ f)) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β → β<VAR>l : FreeAddMonoid α<VAR>b : β<GOAL>l +ᵥ b = List.foldr f b (FreeAddMonoid.toList l)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β → β<VAR>l : FreeMonoid α<VAR>b : β<GOAL>l • b = List.foldr f b (FreeMonoid.toList l)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β → β<VAR>l : List α<VAR>b : β<GOAL>FreeMonoid.ofList l • b = List.foldr f b l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β → β<VAR>l : List α<VAR>b : β<GOAL>FreeAddMonoid.ofList l +ᵥ b = List.foldr f b l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β → β<VAR>x : α<VAR>y : β<GOAL>FreeMonoid.of x • y = f x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β → β<VAR>x : α<VAR>y : β<GOAL>FreeAddMonoid.of x +ᵥ y = f x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>x : α<GOAL>(FreeAddMonoid.map f) (FreeAddMonoid.of x) = FreeAddMonoid.of (f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>x : α<GOAL>(FreeMonoid.map f) (FreeMonoid.of x) = FreeMonoid.of (f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>xs : FreeMonoid α<GOAL>FreeMonoid.toList ((FreeMonoid.map f) xs) = List.map f (FreeMonoid.toList xs)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>xs : FreeAddMonoid α<GOAL>FreeAddMonoid.toList ((FreeAddMonoid.map f) xs) = List.map f (FreeAddMonoid.toList xs)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>xs : List α<GOAL>FreeMonoid.ofList (List.map f xs) = (FreeMonoid.map f) (FreeMonoid.ofList xs)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>xs : List α<GOAL>FreeAddMonoid.ofList (List.map f xs) = (FreeAddMonoid.map f) (FreeAddMonoid.ofList xs)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<GOAL>(FreeAddMonoid.lift fun x => FreeAddMonoid.of (f x)) = FreeAddMonoid.map f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<GOAL>(FreeMonoid.lift fun x => FreeMonoid.of (f x)) = FreeMonoid.map f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>g : β → γ<VAR>f : α → β<GOAL>FreeMonoid.map (g ∘ f) = (FreeMonoid.map g).comp (FreeMonoid.map f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>g : β → γ<VAR>f : α → β<GOAL>FreeAddMonoid.map (g ∘ f) = (FreeAddMonoid.map g).comp (FreeAddMonoid.map f)
<VAR>α : Type u_1<GOAL>FreeMonoid.map id = MonoidHom.id (FreeMonoid α)
<VAR>α : Type u_1<GOAL>FreeAddMonoid.map id = AddMonoidHom.id (FreeAddMonoid α)
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>x : α<GOAL>(FreeAddMonoid.countP p) (FreeAddMonoid.of x) = if p x = (true = true) then 1 else 0
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>l : FreeAddMonoid α<GOAL>(FreeAddMonoid.countP p) l = List.countP (fun b => decide (p b)) l
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>x y : α<GOAL>(FreeAddMonoid.count x) (FreeAddMonoid.of y) = Pi.single x 1 y
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>x : α<VAR>l : FreeAddMonoid α<GOAL>(FreeAddMonoid.count x) l = List.count x l
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>x : α<GOAL>(FreeMonoid.countP p) (FreeMonoid.of x) = if p x then Multiplicative.ofAdd 1 else Multiplicative.ofAdd 0
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>x : α<GOAL>(FreeMonoid.countP p) (FreeMonoid.of x) = if p x then Multiplicative.ofAdd 1 else 1
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>l : FreeAddMonoid α<GOAL>(FreeMonoid.countP p) l = Multiplicative.ofAdd (List.countP (fun b => decide (p b)) l)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>x : α<VAR>l : FreeAddMonoid α<GOAL>(FreeMonoid.count x) l = Multiplicative.ofAdd (List.count x l)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>x y : α<GOAL>(FreeMonoid.count x) (FreeMonoid.of y) = Pi.mulSingle x (Multiplicative.ofAdd 1) y
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>StarMul R<VAR>α : Type u_2<VAR>s : Finset α<VAR>f : α → R<GOAL>star (∏ x ∈ s, f x) = ∏ x ∈ s, star (f x)
<VAR>R : Type u_1<VAR>AddCommMonoid R<VAR>StarAddMonoid R<VAR>α : Type u_2<VAR>s : Finset α<VAR>f : α → R<GOAL>star (∑ x ∈ s, f x) = ∑ x ∈ s, star (f x)
<VAR>M : Type v<VAR>Mul M<VAR>Star M<VAR>self : SubStarSemigroup M<VAR>a : M<VAR>_ha : a ∈ self.carrier<GOAL>star a ∈ self.carrier
<VAR>R : Type v<VAR>NonUnitalNonAssocSemiring R<VAR>Star R<VAR>self : NonUnitalStarSubsemiring R<VAR>a : R<VAR>_ha : a ∈ self.carrier<GOAL>star a ∈ self.carrier
<VAR>R : Type v<VAR>NonUnitalNonAssocSemiring R<VAR>StarRing R<VAR>s : NonUnitalStarSubsemiring R<VAR>x : R<GOAL>x ∈ s.carrier ↔ x ∈ s
<VAR>R : Type v<VAR>NonUnitalNonAssocSemiring R<VAR>StarRing R<VAR>S : NonUnitalStarSubsemiring R<VAR>s : Set R<VAR>hs : s = ↑S<GOAL>↑(S.copy s hs) = s
<VAR>R : Type v<VAR>NonUnitalNonAssocSemiring R<VAR>StarRing R<VAR>S : NonUnitalStarSubsemiring R<VAR>s : Set R<VAR>hs : s = ↑S<GOAL>S.copy s hs = S
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>DecidableEq σ<VAR>p : MvPolynomial σ R<GOAL>p.vars = p.degrees.toFinset
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<GOAL>MvPolynomial.vars 0 = ∅
<VAR>R : Type u<VAR>σ : Type u_1<VAR>r : R<VAR>s : σ →₀ ℕ<VAR>CommSemiring R<VAR>h : r ≠ 0<GOAL>((MvPolynomial.monomial s) r).vars = s.support
<VAR>R : Type u<VAR>σ : Type u_1<VAR>r : R<VAR>CommSemiring R<GOAL>(MvPolynomial.C r).vars = ∅
<VAR>R : Type u<VAR>σ : Type u_1<VAR>n : σ<VAR>CommSemiring R<VAR>Nontrivial R<GOAL>(MvPolynomial.X n).vars = {n}
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>p : MvPolynomial σ R<VAR>i : σ<GOAL>i ∈ p.vars ↔ ∃ d ∈ p.support, i ∈ d.support
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>f : MvPolynomial σ R<VAR>x : σ →₀ ℕ<VAR>H : x ∈ f.support<VAR>v : σ<VAR>h : v ∉ f.vars<GOAL>x v = 0
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>DecidableEq σ<VAR>p q : MvPolynomial σ R<GOAL>(p + q).vars ⊆ p.vars ∪ q.vars
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>DecidableEq σ<VAR>h : Disjoint p.vars q.vars<GOAL>(p + q).vars = p.vars ∪ q.vars
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>DecidableEq σ<VAR>φ ψ : MvPolynomial σ R<GOAL>(φ * ψ).vars ⊆ φ.vars ∪ ψ.vars
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<GOAL>MvPolynomial.vars 1 = ∅
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>φ : MvPolynomial σ R<VAR>n : ℕ<GOAL>(φ ^ n).vars ⊆ φ.vars
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>ι : Type u_3<VAR>DecidableEq σ<VAR>s : Finset ι<VAR>f : ι → MvPolynomial σ R<GOAL>(∏ i ∈ s, f i).vars ⊆ s.biUnion fun i => (f i).vars
<VAR>σ : Type u_1<VAR>A : Type u_3<VAR>CommRing A<VAR>IsDomain A<VAR>a : A<VAR>ha : a ≠ 0<VAR>φ : MvPolynomial σ A<GOAL>(MvPolynomial.C a * φ).vars = φ.vars
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>ι : Type u_3<VAR>t : Finset ι<VAR>φ : ι → MvPolynomial σ R<VAR>DecidableEq σ<GOAL>(∑ i ∈ t, φ i).vars ⊆ t.biUnion fun i => (φ i).vars
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>ι : Type u_3<VAR>t : Finset ι<VAR>φ : ι → MvPolynomial σ R<VAR>DecidableEq σ<VAR>h : Pairwise (Disjoint on fun i => (φ i).vars)<GOAL>(∑ i ∈ t, φ i).vars = t.biUnion fun i => (φ i).vars
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>p : MvPolynomial σ R<VAR>CommSemiring S<VAR>f : R →+* S<GOAL>((MvPolynomial.map f) p).vars ⊆ p.vars
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>p : MvPolynomial σ R<VAR>CommSemiring S<VAR>f : R →+* S<VAR>hf : Function.Injective ⇑f<GOAL>((MvPolynomial.map f) p).vars = p.vars
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>i : σ<VAR>e : ℕ<VAR>r : R<VAR>he : e ≠ 0<VAR>hr : r ≠ 0<GOAL>((MvPolynomial.monomial (Finsupp.single i e)) r).vars = {i}
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>p : MvPolynomial σ R<VAR>DecidableEq σ<GOAL>p.vars = p.support.biUnion Finsupp.support
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S<VAR>f : R →+* S<VAR>g : σ → S<VAR>p : MvPolynomial σ R<VAR>hp : ∀ i ∈ p.vars, g i = 0<GOAL>(MvPolynomial.eval₂Hom f g) p = f (MvPolynomial.constantCoeff p)
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>g : σ → S<VAR>p : MvPolynomial σ R<VAR>hp : ∀ i ∈ p.vars, g i = 0<GOAL>(MvPolynomial.aeval g) p = (algebraMap R S) (MvPolynomial.constantCoeff p)
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S<VAR>f₁ f₂ : R →+* S<VAR>g₁ g₂ : σ → S<VAR>p₁ p₂ : MvPolynomial σ R<GOAL>f₁ = f₂ → (∀ i ∈ p₁.vars, i ∈ p₂.vars → g₁ i = g₂ i) → p₁ = p₂ → (MvPolynomial.eval₂Hom f₁ g₁) p₁ = (MvPolynomial.eval₂Hom f₂ g₂) p₂
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S<VAR>f₁ f₂ : MvPolynomial σ R →+* S<VAR>p₁ p₂ : MvPolynomial σ R<VAR>hC : f₁.comp MvPolynomial.C = f₂.comp MvPolynomial.C<VAR>hv : ∀ i ∈ p₁.vars, i ∈ p₂.vars → f₁ (MvPolynomial.X i) = f₂ (MvPolynomial.X i)<VAR>hp : p₁ = p₂<GOAL>f₁ p₁ = f₂ p₂
<VAR>R : Type u<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>CommSemiring R<VAR>p : MvPolynomial σ R<VAR>f : τ → σ<VAR>hfi : Function.Injective f<VAR>hf : ↑p.vars ⊆ Set.range f<GOAL>∃ q, (MvPolynomial.rename f) q = p
<VAR>R : Type u<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>CommSemiring R<VAR>DecidableEq τ<VAR>f : σ → τ<VAR>φ : MvPolynomial σ R<GOAL>((MvPolynomial.rename f) φ).vars ⊆ Finset.image f φ.vars
<VAR>R : Type u<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>CommSemiring R<VAR>f : σ → τ<VAR>φ : MvPolynomial σ R<VAR>j : τ<VAR>h : j ∈ ((MvPolynomial.rename f) φ).vars<GOAL>∃ i ∈ φ.vars, f i = j
<VAR>R : Type u_1<VAR>DivisionSemiring R<VAR>StarRing R<VAR>q : ℚ≥0<GOAL>star ↑q = ↑q
<VAR>R : Type u_1<VAR>DivisionRing R<VAR>StarRing R<VAR>r : ℚ<GOAL>star ↑r = ↑r
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_4<VAR>CommSemiring R<VAR>f : σ → τ<VAR>r : R<GOAL>(MvPolynomial.rename f) (MvPolynomial.C r) = MvPolynomial.C r
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_4<VAR>CommSemiring R<VAR>f : σ → τ<VAR>i : σ<GOAL>(MvPolynomial.rename f) (MvPolynomial.X i) = MvPolynomial.X (f i)
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_4<VAR>S : Type u_5<VAR>CommSemiring R<VAR>CommSemiring S<VAR>f : R →+* S<VAR>g : σ → τ<VAR>p : MvPolynomial σ R<GOAL>(MvPolynomial.map f) ((MvPolynomial.rename g) p) = (MvPolynomial.rename g) ((MvPolynomial.map f) p)
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>α : Type u_3<VAR>R : Type u_4<VAR>CommSemiring R<VAR>f : σ → τ<VAR>g : τ → α<VAR>p : MvPolynomial σ R<GOAL>(MvPolynomial.rename g) ((MvPolynomial.rename f) p) = (MvPolynomial.rename (g ∘ f)) p
<VAR>σ : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>p : MvPolynomial σ R<GOAL>(MvPolynomial.rename id) p = p
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_4<VAR>CommSemiring R<VAR>f : σ → τ<VAR>d : σ →₀ ℕ<VAR>r : R<GOAL>(MvPolynomial.rename f) ((MvPolynomial.monomial d) r) = (MvPolynomial.monomial (Finsupp.mapDomain f d)) r
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_4<VAR>CommSemiring R<VAR>f : σ → τ<VAR>p : MvPolynomial σ R<GOAL>(MvPolynomial.rename f) p = Finsupp.mapDomain (Finsupp.mapDomain f) p
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_4<VAR>CommSemiring R<VAR>f : σ → τ<VAR>hf : Function.Injective f<GOAL>Function.Injective ⇑(MvPolynomial.rename f)
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_4<VAR>CommSemiring R<VAR>f : σ → τ<VAR>hf : Function.Injective f<VAR>r : R<GOAL>(MvPolynomial.killCompl hf) (MvPolynomial.C r) = MvPolynomial.C r
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_4<VAR>CommSemiring R<VAR>f : σ → τ<VAR>hf : Function.Injective f<GOAL>(MvPolynomial.killCompl hf).comp (MvPolynomial.rename f) = AlgHom.id R (MvPolynomial σ R)
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_4<VAR>CommSemiring R<VAR>f : σ → τ<VAR>hf : Function.Injective f<VAR>p : MvPolynomial σ R<GOAL>(MvPolynomial.killCompl hf) ((MvPolynomial.rename f) p) = p
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_4<VAR>CommSemiring R<VAR>f : σ ≃ τ<VAR>a : MvPolynomial σ R<GOAL>(MvPolynomial.renameEquiv R f) a = (MvPolynomial.rename ⇑f) a
<VAR>σ : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<GOAL>MvPolynomial.renameEquiv R (Equiv.refl σ) = AlgEquiv.refl
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_4<VAR>CommSemiring R<VAR>f : σ ≃ τ<GOAL>(MvPolynomial.renameEquiv R f).symm = MvPolynomial.renameEquiv R f.symm
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>α : Type u_3<VAR>R : Type u_4<VAR>CommSemiring R<VAR>e : σ ≃ τ<VAR>f : τ ≃ α<GOAL>(MvPolynomial.renameEquiv R e).trans (MvPolynomial.renameEquiv R f) = MvPolynomial.renameEquiv R (e.trans f)
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_4<VAR>S : Type u_5<VAR>CommSemiring R<VAR>CommSemiring S<VAR>f : R →+* S<VAR>k : σ → τ<VAR>g : τ → S<VAR>p : MvPolynomial σ R<GOAL>MvPolynomial.eval₂ f g ((MvPolynomial.rename k) p) = MvPolynomial.eval₂ f (g ∘ k) p
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_4<VAR>CommSemiring R<VAR>k : σ → τ<VAR>g : τ → R<VAR>p : MvPolynomial σ R<GOAL>(MvPolynomial.eval g) ((MvPolynomial.rename k) p) = (MvPolynomial.eval (g ∘ k)) p
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_4<VAR>S : Type u_5<VAR>CommSemiring R<VAR>CommSemiring S<VAR>f : R →+* S<VAR>k : σ → τ<VAR>g : τ → S<VAR>p : MvPolynomial σ R<GOAL>(MvPolynomial.eval₂Hom f g) ((MvPolynomial.rename k) p) = (MvPolynomial.eval₂Hom f (g ∘ k)) p
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_4<VAR>S : Type u_5<VAR>CommSemiring R<VAR>CommSemiring S<VAR>k : σ → τ<VAR>g : τ → S<VAR>p : MvPolynomial σ R<VAR>Algebra R S<GOAL>(MvPolynomial.aeval g) ((MvPolynomial.rename k) p) = (MvPolynomial.aeval (g ∘ k)) p