ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>p : MvPolynomial σ R<VAR>m : σ →₀ ℕ<VAR>h : MvPolynomial.coeff m p ≠ 0<GOAL>MvPolynomial.coeff m p ∈ p.coeffs
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>p : MvPolynomial σ R<GOAL>0 ∉ p.coeffs
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<GOAL>⇑MvPolynomial.constantCoeff = MvPolynomial.coeff 0
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>r : R<GOAL>MvPolynomial.constantCoeff (MvPolynomial.C r) = r
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>i : σ<GOAL>MvPolynomial.constantCoeff (MvPolynomial.X i) = 0
<VAR>S₁ : Type v<VAR>σ : Type u_1<VAR>CommSemiring S₁<VAR>R : Type u_2<VAR>SMulZeroClass R S₁<VAR>a : R<VAR>f : MvPolynomial σ S₁<GOAL>MvPolynomial.constantCoeff (a • f) = a • MvPolynomial.constantCoeff f
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>DecidableEq σ<VAR>d : σ →₀ ℕ<VAR>r : R<GOAL>MvPolynomial.constantCoeff ((MvPolynomial.monomial d) r) = if d = 0 then r else 0
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<GOAL>MvPolynomial.constantCoeff.comp MvPolynomial.C = RingHom.id R
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<GOAL>MvPolynomial.constantCoeff.comp (algebraMap R (MvPolynomial σ R)) = RingHom.id R
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>p : MvPolynomial σ R<GOAL>∑ v ∈ p.support, (MvPolynomial.monomial v) (MvPolynomial.coeff v p) = p
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>p : MvPolynomial σ R<GOAL>p = ∑ v ∈ p.support, (MvPolynomial.monomial v) (MvPolynomial.coeff v p)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S₁<VAR>g : R →+* S₁<VAR>X : σ → S₁<VAR>f : MvPolynomial σ R<GOAL>MvPolynomial.eval₂ g X f = ∑ d ∈ f.support, g (MvPolynomial.coeff d f) * ∏ i ∈ d.support, X i ^ d i
<VAR>R : Type u<VAR>S₁ : Type v<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S₁<VAR>Fintype σ<VAR>g : R →+* S₁<VAR>X : σ → S₁<VAR>f : MvPolynomial σ R<GOAL>MvPolynomial.eval₂ g X f = ∑ d ∈ f.support, g (MvPolynomial.coeff d f) * ∏ i : σ, X i ^ d i
<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₁<GOAL>MvPolynomial.eval₂ f g 0 = 0
<VAR>R : Type u<VAR>S₁ : Type v<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>f : R →+* S₁<VAR>g : σ → S₁<GOAL>MvPolynomial.eval₂ f g (p + q) = MvPolynomial.eval₂ f g p + MvPolynomial.eval₂ f g q
<VAR>R : Type u<VAR>S₁ : Type v<VAR>σ : Type u_1<VAR>a : R<VAR>s : σ →₀ ℕ<VAR>CommSemiring R<VAR>CommSemiring S₁<VAR>f : R →+* S₁<VAR>g : σ → S₁<GOAL>MvPolynomial.eval₂ f g ((MvPolynomial.monomial s) a) = f a * s.prod fun n e => g n ^ e
<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>a : R<GOAL>MvPolynomial.eval₂ f g (MvPolynomial.C a) = f a
<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₁<GOAL>MvPolynomial.eval₂ f g 1 = 1
<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>n : σ<GOAL>MvPolynomial.eval₂ f g (MvPolynomial.X n) = g n
<VAR>R : Type u<VAR>S₁ : Type v<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S₁<VAR>p : MvPolynomial σ R<VAR>f : R →+* S₁<VAR>g : σ → S₁<VAR>s : σ →₀ ℕ<VAR>a : R<GOAL>MvPolynomial.eval₂ f g (p * (MvPolynomial.monomial s) a) = MvPolynomial.eval₂ f g p * f a * s.prod fun n e => g n ^ e
<VAR>R : Type u<VAR>S₁ : Type v<VAR>σ : Type u_1<VAR>a : R<VAR>CommSemiring R<VAR>CommSemiring S₁<VAR>p : MvPolynomial σ R<VAR>f : R →+* S₁<VAR>g : σ → S₁<GOAL>MvPolynomial.eval₂ f g (p * MvPolynomial.C a) = MvPolynomial.eval₂ f g p * f a
<VAR>R : Type u<VAR>S₁ : Type v<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S₁<VAR>q : MvPolynomial σ R<VAR>f : R →+* S₁<VAR>g : σ → S₁<VAR>p : MvPolynomial σ R<GOAL>MvPolynomial.eval₂ f g (p * q) = MvPolynomial.eval₂ f g p * MvPolynomial.eval₂ f g q
<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>n : ℕ<GOAL>MvPolynomial.eval₂ f g (p ^ n) = MvPolynomial.eval₂ f g p ^ n
<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₁<GOAL>⇑(MvPolynomial.eval₂Hom f g) = MvPolynomial.eval₂ f g
<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₂ → g₁ = g₂ → 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 : R →+* S₁<VAR>g : σ → S₁<VAR>r : R<GOAL>(MvPolynomial.eval₂Hom f g) (MvPolynomial.C r) = f r
<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>i : σ<GOAL>(MvPolynomial.eval₂Hom f g) (MvPolynomial.X i) = g i
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S₁<VAR>CommSemiring S₂<VAR>f : R →+* S₁<VAR>g : σ → S₁<VAR>φ : S₁ →+* S₂<GOAL>φ.comp (MvPolynomial.eval₂Hom f g) = MvPolynomial.eval₂Hom (φ.comp f) fun i => φ (g i)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S₁<VAR>CommSemiring S₂<VAR>f : R →+* S₁<VAR>g : σ → S₁<VAR>φ : S₁ →+* S₂<VAR>p : MvPolynomial σ R<GOAL>φ ((MvPolynomial.eval₂Hom f g) p) = (MvPolynomial.eval₂Hom (φ.comp f) fun i => φ (g i)) p
<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>d : σ →₀ ℕ<VAR>r : R<GOAL>(MvPolynomial.eval₂Hom f g) ((MvPolynomial.monomial d) r) = f r * d.prod fun i k => g i ^ k
<VAR>R : Type u<VAR>S₁ : Type v<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S₁<VAR>S₂ : Type u_2<VAR>CommSemiring S₂<VAR>k : S₁ →+* S₂<VAR>f : R →+* S₁<VAR>g : σ → S₁<VAR>p : MvPolynomial σ R<GOAL>k (MvPolynomial.eval₂ f g p) = MvPolynomial.eval₂ (k.comp f) (⇑k ∘ g) p
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>p : MvPolynomial σ R<GOAL>MvPolynomial.eval₂ MvPolynomial.C MvPolynomial.X p = p
<VAR>R : Type u<VAR>S₁ : Type v<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S₁<VAR>p : MvPolynomial σ R<VAR>f : R →+* S₁<VAR>g₁ g₂ : σ → S₁<VAR>h : ∀ {i : σ} {c : σ →₀ ℕ}, i ∈ c.support → MvPolynomial.coeff c p ≠ 0 → g₁ i = g₂ i<GOAL>MvPolynomial.eval₂ f g₁ p = MvPolynomial.eval₂ f g₂ p
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S₁<VAR>f : R →+* S₁<VAR>g : σ → S₁<VAR>s : Finset S₂<VAR>p : S₂ → MvPolynomial σ R<GOAL>MvPolynomial.eval₂ f g (∑ x ∈ s, p x) = ∑ x ∈ s, MvPolynomial.eval₂ f g (p x)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S₁<VAR>f : R →+* S₁<VAR>g : σ → S₁<VAR>s : Finset S₂<VAR>p : S₂ → MvPolynomial σ R<GOAL>MvPolynomial.eval₂ f g (∏ x ∈ s, p x) = ∏ x ∈ s, MvPolynomial.eval₂ f g (p x)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S₁<VAR>f : R →+* S₁<VAR>g : σ → S₁<VAR>q : S₂ → MvPolynomial σ R<VAR>p : MvPolynomial S₂ R<GOAL>MvPolynomial.eval₂ f (fun t => MvPolynomial.eval₂ f g (q t)) p = MvPolynomial.eval₂ f g (MvPolynomial.eval₂ MvPolynomial.C q p)
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>X : σ → R<VAR>f : MvPolynomial σ R<GOAL>(MvPolynomial.eval X) f = ∑ d ∈ f.support, MvPolynomial.coeff d f * ∏ i ∈ d.support, X i ^ d i
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>Fintype σ<VAR>X : σ → R<VAR>f : MvPolynomial σ R<GOAL>(MvPolynomial.eval X) f = ∑ d ∈ f.support, MvPolynomial.coeff d f * ∏ i : σ, X i ^ d i
<VAR>R : Type u<VAR>σ : Type u_1<VAR>a : R<VAR>s : σ →₀ ℕ<VAR>CommSemiring R<VAR>f : σ → R<GOAL>(MvPolynomial.eval f) ((MvPolynomial.monomial s) a) = a * s.prod fun n e => f n ^ e
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>f : σ → R<VAR>a : R<GOAL>(MvPolynomial.eval f) (MvPolynomial.C a) = a
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>f : σ → R<VAR>n : σ<GOAL>(MvPolynomial.eval f) (MvPolynomial.X n) = f n
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>x : σ → R<VAR>p : MvPolynomial σ R<VAR>s : R<GOAL>(MvPolynomial.eval x) (s • p) = s * (MvPolynomial.eval x) p
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>f : σ → R<GOAL>(MvPolynomial.eval f) (p + q) = (MvPolynomial.eval f) p + (MvPolynomial.eval f) q
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>f : σ → R<GOAL>(MvPolynomial.eval f) (p * q) = (MvPolynomial.eval f) p * (MvPolynomial.eval f) q
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>p : MvPolynomial σ R<VAR>f : σ → R<VAR>n : ℕ<GOAL>(MvPolynomial.eval f) (p ^ n) = (MvPolynomial.eval f) p ^ n
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>f : ι → MvPolynomial σ R<VAR>g : σ → R<GOAL>(MvPolynomial.eval g) (∑ i ∈ s, f i) = ∑ i ∈ s, (MvPolynomial.eval g) (f i)
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>f : ι → MvPolynomial σ R<VAR>g : σ → R<GOAL>(MvPolynomial.eval g) (∏ i ∈ s, f i) = ∏ i ∈ s, (MvPolynomial.eval g) (f i)
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>τ : Type u_2<VAR>f : σ → MvPolynomial τ R<VAR>g : τ → R<VAR>p : MvPolynomial σ R<GOAL>(MvPolynomial.eval (⇑(MvPolynomial.eval g) ∘ f)) p = (MvPolynomial.eval g) (MvPolynomial.eval₂ MvPolynomial.C f p)
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>g : σ → R<VAR>p : MvPolynomial σ R<GOAL>MvPolynomial.eval₂ (RingHom.id R) g p = (MvPolynomial.eval g) p
<VAR>R : Type u<VAR>σ : Type u_1<VAR>S : Type u_2<VAR>τ : Type u_3<VAR>x : τ → S<VAR>CommSemiring R<VAR>CommSemiring S<VAR>f : R →+* MvPolynomial τ S<VAR>g : σ → MvPolynomial τ S<VAR>p : MvPolynomial σ R<GOAL>(MvPolynomial.eval x) (MvPolynomial.eval₂ f g p) = MvPolynomial.eval₂ ((MvPolynomial.eval x).comp f) (fun s => (MvPolynomial.eval x) (g s)) p
<VAR>R : Type u<VAR>S₁ : Type v<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S₁<VAR>f : R →+* S₁<VAR>s : σ →₀ ℕ<VAR>a : R<GOAL>(MvPolynomial.map f) ((MvPolynomial.monomial s) a) = (MvPolynomial.monomial s) (f a)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S₁<VAR>f : R →+* S₁<VAR>a : R<GOAL>(MvPolynomial.map f) (MvPolynomial.C a) = MvPolynomial.C (f a)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S₁<VAR>f : R →+* S₁<VAR>n : σ<GOAL>(MvPolynomial.map f) (MvPolynomial.X n) = MvPolynomial.X n
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>p : MvPolynomial σ R<GOAL>(MvPolynomial.map (RingHom.id R)) p = p
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S₁<VAR>f : R →+* S₁<VAR>CommSemiring S₂<VAR>g : S₁ →+* S₂<VAR>p : MvPolynomial σ R<GOAL>(MvPolynomial.map g) ((MvPolynomial.map f) p) = (MvPolynomial.map (g.comp f)) p
<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<GOAL>MvPolynomial.eval₂ f g p = (MvPolynomial.eval g) ((MvPolynomial.map f) p)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S₁<VAR>S₂ : Type u_2<VAR>CommSemiring S₂<VAR>k : S₁ →+* S₂<VAR>f : R →+* S₁<VAR>g : σ → S₁<VAR>p : MvPolynomial σ R<GOAL>k (MvPolynomial.eval₂ f g p) = MvPolynomial.eval₂ k (⇑k ∘ g) ((MvPolynomial.map f) p)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>CommSemiring R<VAR>CommSemiring S₁<VAR>f : R →+* S₁<VAR>g : S₂ → MvPolynomial S₃ R<VAR>p : MvPolynomial S₂ R<GOAL>(MvPolynomial.map f) (MvPolynomial.eval₂ MvPolynomial.C g p) = MvPolynomial.eval₂ MvPolynomial.C (⇑(MvPolynomial.map f) ∘ g) ((MvPolynomial.map f) p)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S₁<VAR>f : R →+* S₁<VAR>p : MvPolynomial σ R<VAR>m : σ →₀ ℕ<GOAL>MvPolynomial.coeff m ((MvPolynomial.map f) p) = f (MvPolynomial.coeff m p)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S₁<VAR>f : R →+* S₁<VAR>hf : Function.Injective ⇑f<GOAL>Function.Injective ⇑(MvPolynomial.map f)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S₁<VAR>f : R →+* S₁<VAR>hf : Function.Surjective ⇑f<GOAL>Function.Surjective ⇑(MvPolynomial.map f)
<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₁ →+* R<VAR>hf : Function.LeftInverse ⇑f ⇑g<GOAL>Function.LeftInverse ⇑(MvPolynomial.map f) ⇑(MvPolynomial.map g)
<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₁ →+* R<VAR>hf : Function.RightInverse ⇑f ⇑g<GOAL>Function.RightInverse ⇑(MvPolynomial.map f) ⇑(MvPolynomial.map g)
<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<GOAL>(MvPolynomial.eval g) ((MvPolynomial.map f) p) = MvPolynomial.eval₂ f g p
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S₁<VAR>CommSemiring S₂<VAR>f : R →+* S₁<VAR>g : σ → S₂<VAR>φ : S₁ →+* S₂<VAR>p : MvPolynomial σ R<GOAL>MvPolynomial.eval₂ φ g ((MvPolynomial.map f) p) = MvPolynomial.eval₂ (φ.comp f) g p
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S₁<VAR>CommSemiring S₂<VAR>f : R →+* S₁<VAR>g : σ → S₂<VAR>φ : S₁ →+* S₂<VAR>p : MvPolynomial σ R<GOAL>(MvPolynomial.eval₂Hom φ g) ((MvPolynomial.map f) p) = (MvPolynomial.eval₂Hom (φ.comp f) g) p
<VAR>R : Type u<VAR>S₁ : Type v<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S₁<VAR>f : R →+* S₁<VAR>φ : MvPolynomial σ R<GOAL>MvPolynomial.constantCoeff ((MvPolynomial.map f) φ) = f (MvPolynomial.constantCoeff φ)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S₁<VAR>f : R →+* S₁<GOAL>MvPolynomial.constantCoeff.comp (MvPolynomial.map f) = f.comp MvPolynomial.constantCoeff
<VAR>R : Type u<VAR>S₁ : Type v<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S₁<VAR>f : R →+* S₁<VAR>p : MvPolynomial σ R<GOAL>((MvPolynomial.map f) p).support ⊆ p.support
<VAR>R : Type u<VAR>S₁ : Type v<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S₁<VAR>p : MvPolynomial σ R<VAR>f : R →+* S₁<VAR>hf : Function.Injective ⇑f<GOAL>((MvPolynomial.map f) p).support = p.support
<VAR>R : Type u<VAR>S₁ : Type v<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S₁<VAR>q : R →+* S₁<VAR>r : R<VAR>hr : ∀ (r' : R), q r' = 0 ↔ r ∣ r'<VAR>φ : MvPolynomial σ R<GOAL>MvPolynomial.C r ∣ φ ↔ (MvPolynomial.map q) φ = 0
<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₁ → R<VAR>hg : g 0 = 0<VAR>φ : MvPolynomial σ S₁<GOAL>(MvPolynomial.map f) (Finsupp.mapRange g hg φ) = φ ↔ ∀ (d : σ →₀ ℕ), f (g (MvPolynomial.coeff d φ)) = MvPolynomial.coeff d φ
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S₁<VAR>CommSemiring S₂<VAR>Algebra R S₁<VAR>Algebra R S₂<VAR>f : S₁ →ₐ[R] S₂<VAR>p : MvPolynomial σ S₁<GOAL>(MvPolynomial.mapAlgHom f) p = MvPolynomial.eval₂ (MvPolynomial.C.comp ↑f) MvPolynomial.X p
<VAR>R : Type u<VAR>S₁ : Type v<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S₁<VAR>Algebra R S₁<GOAL>MvPolynomial.mapAlgHom (AlgHom.id R S₁) = AlgHom.id R (MvPolynomial σ S₁)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S₁<VAR>CommSemiring S₂<VAR>Algebra R S₁<VAR>Algebra R S₂<VAR>f : S₁ →ₐ[R] S₂<GOAL>↑(MvPolynomial.mapAlgHom f) = MvPolynomial.map ↑f
<VAR>R : Type u<VAR>S₁ : Type v<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S₁<VAR>Algebra R S₁<VAR>r : R<GOAL>(algebraMap R (MvPolynomial σ S₁)) r = MvPolynomial.C ((algebraMap R S₁) r)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S₁<VAR>Algebra R S₁<VAR>f : σ → S₁<VAR>p : MvPolynomial σ R<GOAL>(MvPolynomial.aeval f) p = MvPolynomial.eval₂ (algebraMap R S₁) f p
<VAR>R : Type u<VAR>S₁ : Type v<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S₁<VAR>Algebra R S₁<VAR>f : σ → S₁<VAR>p : MvPolynomial σ R<GOAL>(MvPolynomial.aeval f) p = (MvPolynomial.eval₂Hom (algebraMap R S₁) f) p
<VAR>S₁ : Type v<VAR>σ : Type u_1<VAR>CommSemiring S₁<VAR>f : σ → S₁<GOAL>↑(MvPolynomial.aeval f) = MvPolynomial.eval f
<VAR>R : Type u<VAR>S₁ : Type v<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S₁<VAR>Algebra R S₁<VAR>f : σ → S₁<VAR>s : σ<GOAL>(MvPolynomial.aeval f) (MvPolynomial.X s) = f s
<VAR>R : Type u<VAR>S₁ : Type v<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S₁<VAR>Algebra R S₁<VAR>f : σ → S₁<VAR>r : R<GOAL>(MvPolynomial.aeval f) (MvPolynomial.C r) = (algebraMap R S₁) r
<VAR>R : Type u<VAR>S₁ : Type v<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S₁<VAR>Algebra R S₁<VAR>φ : MvPolynomial σ R →ₐ[R] S₁<GOAL>φ = MvPolynomial.aeval (⇑φ ∘ MvPolynomial.X)
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<GOAL>MvPolynomial.aeval MvPolynomial.X = AlgHom.id R (MvPolynomial σ R)
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>p : MvPolynomial σ R<GOAL>(MvPolynomial.aeval MvPolynomial.X) p = p
<VAR>R : Type u<VAR>S₁ : Type v<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S₁<VAR>Algebra R S₁<VAR>f : σ → S₁<VAR>B : Type u_2<VAR>CommSemiring B<VAR>Algebra R B<VAR>φ : S₁ →ₐ[R] B<GOAL>φ.comp (MvPolynomial.aeval f) = MvPolynomial.aeval fun i => φ (f i)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S₁<VAR>Algebra R S₁<VAR>B : Type u_2<VAR>CommSemiring B<VAR>g : σ → S₁<VAR>φ : S₁ →+* B<VAR>p : MvPolynomial σ R<GOAL>φ ((MvPolynomial.aeval g) p) = (MvPolynomial.eval₂Hom (φ.comp (algebraMap R S₁)) fun i => φ (g i)) p
<VAR>R : Type u<VAR>S₂ : Type w<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S₂<VAR>f : R →+* S₂<GOAL>MvPolynomial.eval₂Hom f 0 = f.comp MvPolynomial.constantCoeff
<VAR>R : Type u<VAR>S₂ : Type w<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S₂<VAR>f : R →+* S₂<GOAL>(MvPolynomial.eval₂Hom f fun x => 0) = f.comp MvPolynomial.constantCoeff
<VAR>R : Type u<VAR>S₂ : Type w<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S₂<VAR>f : R →+* S₂<VAR>p : MvPolynomial σ R<GOAL>(MvPolynomial.eval₂Hom f 0) p = f (MvPolynomial.constantCoeff p)
<VAR>R : Type u<VAR>S₂ : Type w<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S₂<VAR>f : R →+* S₂<VAR>p : MvPolynomial σ R<GOAL>(MvPolynomial.eval₂Hom f fun x => 0) p = f (MvPolynomial.constantCoeff p)
<VAR>R : Type u<VAR>S₂ : Type w<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S₂<VAR>f : R →+* S₂<VAR>p : MvPolynomial σ R<GOAL>MvPolynomial.eval₂ f 0 p = f (MvPolynomial.constantCoeff p)
<VAR>R : Type u<VAR>S₂ : Type w<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S₂<VAR>f : R →+* S₂<VAR>p : MvPolynomial σ R<GOAL>MvPolynomial.eval₂ f (fun x => 0) 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>p : MvPolynomial σ R<GOAL>(MvPolynomial.aeval 0) 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>Algebra R S₁<VAR>p : MvPolynomial σ R<GOAL>(MvPolynomial.aeval fun x => 0) p = (algebraMap R S₁) (MvPolynomial.constantCoeff p)
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<GOAL>MvPolynomial.eval 0 = MvPolynomial.constantCoeff
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<GOAL>(MvPolynomial.eval fun x => 0) = MvPolynomial.constantCoeff
<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>d : σ →₀ ℕ<VAR>r : R<GOAL>(MvPolynomial.aeval g) ((MvPolynomial.monomial d) r) = (algebraMap R S₁) r * d.prod fun i k => g i ^ k
<VAR>R : Type u<VAR>S₂ : Type w<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S₂<VAR>f : R →+* S₂<VAR>g : σ → S₂<VAR>φ : MvPolynomial σ R<VAR>h : ∀ (d : σ →₀ ℕ), MvPolynomial.coeff d φ ≠ 0 → ∃ i ∈ d.support, g i = 0<GOAL>(MvPolynomial.eval₂Hom f g) φ = 0
<VAR>R : Type u<VAR>S₂ : Type w<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S₂<VAR>Algebra R S₂<VAR>f : σ → S₂<VAR>φ : MvPolynomial σ R<VAR>h : ∀ (d : σ →₀ ℕ), MvPolynomial.coeff d φ ≠ 0 → ∃ i ∈ d.support, f i = 0<GOAL>(MvPolynomial.aeval f) φ = 0
<VAR>R : Type u<VAR>S₁ : Type v<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S₁<VAR>Algebra R S₁<VAR>f : σ → S₁<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>φ : ι → MvPolynomial σ R<GOAL>(MvPolynomial.aeval f) (∑ i ∈ s, φ i) = ∑ i ∈ s, (MvPolynomial.aeval f) (φ i)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S₁<VAR>Algebra R S₁<VAR>f : σ → S₁<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>φ : ι → MvPolynomial σ R<GOAL>(MvPolynomial.aeval f) (∏ i ∈ s, φ i) = ∏ i ∈ s, (MvPolynomial.aeval f) (φ i)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S₁<VAR>Algebra R S₁<VAR>f : σ → S₁<GOAL>Algebra.adjoin R (Set.range f) = (MvPolynomial.aeval f).range
<VAR>R : Type u<VAR>S₁ : Type v<VAR>CommSemiring R<VAR>CommSemiring S₁<VAR>Algebra R S₁<VAR>s : Set S₁<GOAL>Algebra.adjoin R s = (MvPolynomial.aeval Subtype.val).range
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>S : Type u_2<VAR>A : Type u_3<VAR>CommSemiring S<VAR>CommSemiring A<VAR>Algebra S R<VAR>Algebra S A<VAR>g : R →ₐ[S] A<VAR>y : σ → A<VAR>i : σ<GOAL>(MvPolynomial.aevalTower g y) (MvPolynomial.X i) = y i
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>S : Type u_2<VAR>A : Type u_3<VAR>CommSemiring S<VAR>CommSemiring A<VAR>Algebra S R<VAR>Algebra S A<VAR>g : R →ₐ[S] A<VAR>y : σ → A<VAR>x : R<GOAL>(MvPolynomial.aevalTower g y) (MvPolynomial.C x) = g x
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>S : Type u_2<VAR>A : Type u_3<VAR>CommSemiring S<VAR>CommSemiring A<VAR>Algebra S R<VAR>Algebra S A<VAR>g : R →ₐ[S] A<VAR>y : σ → A<GOAL>(↑(MvPolynomial.aevalTower g y)).comp MvPolynomial.C = ↑g
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>S : Type u_2<VAR>A : Type u_3<VAR>CommSemiring S<VAR>CommSemiring A<VAR>Algebra S R<VAR>Algebra S A<VAR>g : R →ₐ[S] A<VAR>y : σ → A<VAR>x : R<GOAL>(MvPolynomial.aevalTower g y) ((algebraMap R (MvPolynomial σ R)) x) = g x
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>S : Type u_2<VAR>A : Type u_3<VAR>CommSemiring S<VAR>CommSemiring A<VAR>Algebra S R<VAR>Algebra S A<VAR>g : R →ₐ[S] A<VAR>y : σ → A<GOAL>(↑(MvPolynomial.aevalTower g y)).comp (algebraMap R (MvPolynomial σ R)) = ↑g
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>S : Type u_2<VAR>A : Type u_3<VAR>CommSemiring S<VAR>CommSemiring A<VAR>Algebra S R<VAR>Algebra S A<VAR>g : R →ₐ[S] A<VAR>y : σ → A<VAR>x : R<GOAL>(MvPolynomial.aevalTower g y) ((IsScalarTower.toAlgHom S R (MvPolynomial σ R)) x) = g x
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>S : Type u_2<VAR>A : Type u_3<VAR>CommSemiring S<VAR>CommSemiring A<VAR>Algebra S R<VAR>Algebra S A<VAR>g : R →ₐ[S] A<VAR>y : σ → A<GOAL>(MvPolynomial.aevalTower g y).comp (IsScalarTower.toAlgHom S R (MvPolynomial σ R)) = g
<VAR>σ : Type u_1<VAR>S : Type u_2<VAR>CommSemiring S<GOAL>MvPolynomial.aevalTower (AlgHom.id S S) = MvPolynomial.aeval
<VAR>σ : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>CommSemiring S<VAR>CommSemiring A<VAR>Algebra S A<GOAL>MvPolynomial.aevalTower (Algebra.ofId S A) = MvPolynomial.aeval
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>S : Type u_2<VAR>subS : Type u_3<VAR>CommSemiring S<VAR>SetLike subS S<VAR>SubsemiringClass subS S<VAR>f : R →+* S<VAR>p : MvPolynomial σ R<VAR>s : subS<VAR>hs : ∀ i ∈ p.support, f (MvPolynomial.coeff i p) ∈ s<VAR>v : σ → S<VAR>hv : ∀ (i : σ), v i ∈ s<GOAL>MvPolynomial.eval₂ f v p ∈ s
<VAR>σ : Type u_1<VAR>S : Type u_2<VAR>subS : Type u_3<VAR>CommSemiring S<VAR>SetLike subS S<VAR>SubsemiringClass subS S<VAR>p : MvPolynomial σ S<VAR>s : subS<VAR>hs : ∀ i ∈ p.support, MvPolynomial.coeff i p ∈ s<VAR>v : σ → S<VAR>hv : ∀ (i : σ), v i ∈ s<GOAL>(MvPolynomial.eval v) p ∈ s