ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>CommRing R<VAR>X Y Z : Type v<VAR>AddCommGroup X<VAR>Module R X<VAR>AddCommGroup Y<VAR>Module R Y<VAR>AddCommGroup Z<VAR>Module R Z<VAR>Coalgebra R X<VAR>Coalgebra R Y<VAR>Coalgebra R Z<VAR>e : X ≃ₗc[R] Y<VAR>f : Y ≃ₗc[R] Z<GOAL>(e.trans f).toCoalgebraCatIso = e.toCoalgebraCatIso ≪≫ f.toCoalgebraCatIso
<VAR>R : Type u<VAR>CommRing R<VAR>X Y : CoalgebraCat R<VAR>i : X ≅ Y<GOAL>↑i.toCoalgEquiv = i.hom.toCoalgHom
<VAR>R : Type u<VAR>CommRing R<VAR>X : CoalgebraCat R<GOAL>(CategoryTheory.Iso.refl X).toCoalgEquiv = CoalgEquiv.refl R ↑X.toModuleCat
<VAR>R : Type u<VAR>CommRing R<VAR>X Y : CoalgebraCat R<VAR>e : X ≅ Y<GOAL>e.symm.toCoalgEquiv = e.toCoalgEquiv.symm
<VAR>R : Type u<VAR>CommRing R<VAR>X Y Z : CoalgebraCat R<VAR>e : X ≅ Y<VAR>f : Y ≅ Z<GOAL>(e ≪≫ f).toCoalgEquiv = e.toCoalgEquiv.trans f.toCoalgEquiv
<VAR>R : Type u<VAR>Ring R<VAR>P : Type (max u v)<VAR>AddCommGroup P<VAR>Module R P<GOAL>Module.Projective R P ↔ CategoryTheory.Projective (ModuleCat.of R P)
<VAR>R : Type u<VAR>Ring R<VAR>M : ModuleCat R<VAR>ι : Type u'<VAR>b : Basis ι R ↑M<GOAL>CategoryTheory.Projective M
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<GOAL>CategoryTheory.Simple (ModuleCat.of R M) ↔ IsSimpleModule R M
<VAR>R : Type u_1<VAR>Ring R<VAR>M : ModuleCat R<GOAL>CategoryTheory.Simple M ↔ IsSimpleModule R ↑M
<VAR>R : Type u_1<VAR>Ring R<VAR>k : Type u_3<VAR>Field k<VAR>Algebra k R<VAR>V : ModuleCat R<VAR>h : FiniteDimensional.finrank k ↑V = 1<GOAL>CategoryTheory.Simple V
<VAR>R : Type u<VAR>CommRing R<VAR>X : Type v<VAR>Ring X<VAR>Bialgebra R X<GOAL>(BialgebraCat.of R X).instBialgebra = inferInstance
<VAR>R : Type u<VAR>CommRing R<VAR>X : Type v<VAR>Ring X<VAR>Bialgebra R X<GOAL>(BialgebraCat.of R X).str = inferInstance
<VAR>R : Type u<VAR>CommRing R<VAR>X : Type v<VAR>Ring X<VAR>Bialgebra R X<GOAL>↑(BialgebraCat.of R X).toBundled = X
<VAR>R : Type u<VAR>CommRing R<VAR>X : Type v<VAR>Ring X<VAR>Bialgebra R X<GOAL>Coalgebra.comul = Coalgebra.comul
<VAR>R : Type u<VAR>CommRing R<VAR>X : Type v<VAR>Ring X<VAR>Bialgebra R X<GOAL>Coalgebra.counit = Coalgebra.counit
<VAR>R : Type u<VAR>CommRing R<VAR>V W : BialgebraCat R<GOAL>Function.Injective BialgebraCat.Hom.toBialgHom
<VAR>R : Type u<VAR>CommRing R<VAR>X Y : BialgebraCat R<VAR>f g : X ⟶ Y<VAR>h : f.toBialgHom = g.toBialgHom<GOAL>f = g
<VAR>R : Type u<VAR>CommRing R<VAR>X Y Z : BialgebraCat R<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(f ≫ g).toBialgHom = g.toBialgHom.comp f.toBialgHom
<VAR>R : Type u<VAR>CommRing R<VAR>M : BialgebraCat R<GOAL>(𝟙 M).toBialgHom = BialgHom.id R ↑M.toBundled
<VAR>R : Type u<VAR>CommRing R<VAR>X : BialgebraCat R<GOAL>(CategoryTheory.forget₂ (BialgebraCat R) (AlgebraCat R)).obj X = AlgebraCat.of R ↑X.toBundled
<VAR>R : Type u<VAR>CommRing R<VAR>X Y : BialgebraCat R<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.forget₂ (BialgebraCat R) (AlgebraCat R)).map f = ↑f.toBialgHom
<VAR>R : Type u<VAR>CommRing R<VAR>X : BialgebraCat R<GOAL>(CategoryTheory.forget₂ (BialgebraCat R) (CoalgebraCat R)).obj X = CoalgebraCat.of R ↑X.toBundled
<VAR>R : Type u<VAR>CommRing R<VAR>X Y : BialgebraCat R<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.forget₂ (BialgebraCat R) (CoalgebraCat R)).map f = CoalgebraCat.ofHom ↑f.toBialgHom
<VAR>R : Type u<VAR>CommRing R<VAR>X Y : Type v<VAR>Ring X<VAR>Ring Y<VAR>Bialgebra R X<VAR>Bialgebra R Y<VAR>e : X ≃ₐc[R] Y<GOAL>e.toBialgebraCatIso.hom.toBialgHom = ↑e
<VAR>R : Type u<VAR>CommRing R<VAR>X Y : Type v<VAR>Ring X<VAR>Ring Y<VAR>Bialgebra R X<VAR>Bialgebra R Y<VAR>e : X ≃ₐc[R] Y<GOAL>e.toBialgebraCatIso.inv.toBialgHom = ↑e.symm
<VAR>R : Type u<VAR>CommRing R<VAR>X : Type v<VAR>Ring X<VAR>Bialgebra R X<GOAL>(BialgEquiv.refl R X).toBialgebraCatIso = CategoryTheory.Iso.refl (BialgebraCat.of R X)
<VAR>R : Type u<VAR>CommRing R<VAR>X Y : Type v<VAR>Ring X<VAR>Ring Y<VAR>Bialgebra R X<VAR>Bialgebra R Y<VAR>e : X ≃ₐc[R] Y<GOAL>e.symm.toBialgebraCatIso = e.toBialgebraCatIso.symm
<VAR>R : Type u<VAR>CommRing R<VAR>X Y Z : Type v<VAR>Ring X<VAR>Ring Y<VAR>Ring Z<VAR>Bialgebra R X<VAR>Bialgebra R Y<VAR>Bialgebra R Z<VAR>e : X ≃ₐc[R] Y<VAR>f : Y ≃ₐc[R] Z<GOAL>(e.trans f).toBialgebraCatIso = e.toBialgebraCatIso ≪≫ f.toBialgebraCatIso
<VAR>R : Type u<VAR>CommRing R<VAR>X Y : BialgebraCat R<VAR>i : X ≅ Y<GOAL>↑i.toBialgEquiv = i.hom.toBialgHom
<VAR>R : Type u<VAR>CommRing R<VAR>X : BialgebraCat R<GOAL>(CategoryTheory.Iso.refl X).toBialgEquiv = BialgEquiv.refl R ↑X.toBundled
<VAR>R : Type u<VAR>CommRing R<VAR>X Y : BialgebraCat R<VAR>e : X ≅ Y<GOAL>e.symm.toBialgEquiv = e.toBialgEquiv.symm
<VAR>R : Type u<VAR>CommRing R<VAR>X Y Z : BialgebraCat R<VAR>e : X ≅ Y<VAR>f : Y ≅ Z<GOAL>(e ≪≫ f).toBialgEquiv = e.toBialgEquiv.trans f.toBialgEquiv
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>s : σ →₀ ℕ<VAR>a : R<GOAL>Finsupp.single s a = (MvPolynomial.monomial s) a
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>p q : MvPolynomial σ R<GOAL>p * q = Finsupp.sum p fun m a => Finsupp.sum q fun n b => (MvPolynomial.monomial (m + n)) (a * b)
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<GOAL>algebraMap R (MvPolynomial σ R) = MvPolynomial.C
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>r : R<VAR>hr : r ≠ 0<GOAL>Function.Injective fun s => (MvPolynomial.monomial s) r
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>s t : σ →₀ ℕ<VAR>r : R<VAR>hr : r ≠ 0<GOAL>(MvPolynomial.monomial s) r = (MvPolynomial.monomial t) r ↔ s = t
<VAR>R : Type u<VAR>σ : Type u_1<VAR>a : R<VAR>CommSemiring R<GOAL>MvPolynomial.C a = (MvPolynomial.monomial 0) a
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<GOAL>MvPolynomial.C 0 = 0
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<GOAL>MvPolynomial.C 1 = 1
<VAR>R : Type u<VAR>σ : Type u_1<VAR>a a' : R<VAR>s : σ →₀ ℕ<VAR>CommSemiring R<GOAL>MvPolynomial.C a * (MvPolynomial.monomial s) a' = (MvPolynomial.monomial s) (a * a')
<VAR>R : Type u<VAR>σ : Type u_1<VAR>a a' : R<VAR>CommSemiring R<GOAL>MvPolynomial.C (a + a') = MvPolynomial.C a + MvPolynomial.C a'
<VAR>R : Type u<VAR>σ : Type u_1<VAR>a a' : R<VAR>CommSemiring R<GOAL>MvPolynomial.C (a * a') = MvPolynomial.C a * MvPolynomial.C a'
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>a : R<VAR>n : ℕ<GOAL>MvPolynomial.C (a ^ n) = MvPolynomial.C a ^ n
<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>CommSemiring R<GOAL>Function.Injective ⇑MvPolynomial.C
<VAR>R : Type u_2<VAR>CommSemiring R<VAR>σ : Type u_3<VAR>IsEmpty σ<GOAL>Function.Surjective ⇑MvPolynomial.C
<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>CommSemiring R<VAR>r s : R<GOAL>MvPolynomial.C r = MvPolynomial.C s ↔ r = s
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>n : ℕ<GOAL>MvPolynomial.C ↑n = ↑n
<VAR>R : Type u<VAR>σ : Type u_1<VAR>a : R<VAR>CommSemiring R<VAR>p : MvPolynomial σ R<GOAL>MvPolynomial.C a * p = a • p
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>p : MvPolynomial σ R<VAR>a : R<GOAL>a • p = MvPolynomial.C a * p
<VAR>R : Type u<VAR>σ : Type u_1<VAR>a : R<VAR>CommSemiring R<GOAL>MvPolynomial.C a = a • 1
<VAR>R : Type u<VAR>σ : Type u_1<VAR>a : R<VAR>s : σ →₀ ℕ<VAR>CommSemiring R<VAR>S₁ : Type u_2<VAR>SMulZeroClass S₁ R<VAR>r : S₁<GOAL>r • (MvPolynomial.monomial s) a = (MvPolynomial.monomial s) (r • a)
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>Nontrivial R<GOAL>Function.Injective MvPolynomial.X
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>Nontrivial R<VAR>m n : σ<GOAL>MvPolynomial.X m = MvPolynomial.X n ↔ m = n
<VAR>R : Type u<VAR>σ : Type u_1<VAR>a : R<VAR>e : ℕ<VAR>s : σ →₀ ℕ<VAR>CommSemiring R<GOAL>(MvPolynomial.monomial s) a ^ e = (MvPolynomial.monomial (e • s)) (a ^ e)
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>s s' : σ →₀ ℕ<VAR>a b : R<GOAL>(MvPolynomial.monomial s) a * (MvPolynomial.monomial s') b = (MvPolynomial.monomial (s + s')) (a * b)
<VAR>R : Type u<VAR>σ : Type u_1<VAR>s : σ →₀ ℕ<VAR>CommSemiring R<GOAL>(MvPolynomial.monomialOneHom R σ) s = (MvPolynomial.monomial s) 1
<VAR>R : Type u<VAR>σ : Type u_1<VAR>e : ℕ<VAR>n : σ<VAR>CommSemiring R<GOAL>MvPolynomial.X n ^ e = (MvPolynomial.monomial (Finsupp.single n e)) 1
<VAR>R : Type u<VAR>σ : Type u_1<VAR>a : R<VAR>e : ℕ<VAR>n : σ<VAR>s : σ →₀ ℕ<VAR>CommSemiring R<GOAL>(MvPolynomial.monomial (s + Finsupp.single n e)) a = (MvPolynomial.monomial s) a * MvPolynomial.X n ^ e
<VAR>R : Type u<VAR>σ : Type u_1<VAR>a : R<VAR>e : ℕ<VAR>n : σ<VAR>s : σ →₀ ℕ<VAR>CommSemiring R<GOAL>(MvPolynomial.monomial (Finsupp.single n e + s)) a = MvPolynomial.X n ^ e * (MvPolynomial.monomial s) a
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>s : σ<VAR>a : R<VAR>n : ℕ<GOAL>MvPolynomial.C a * MvPolynomial.X s ^ n = (MvPolynomial.monomial (Finsupp.single s n)) a
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>s : σ<VAR>a : R<GOAL>MvPolynomial.C a * MvPolynomial.X s = (MvPolynomial.monomial (Finsupp.single s 1)) a
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>s : σ →₀ ℕ<GOAL>(MvPolynomial.monomial s) 0 = 0
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<GOAL>⇑(MvPolynomial.monomial 0) = ⇑MvPolynomial.C
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>s : σ →₀ ℕ<VAR>b : R<GOAL>(MvPolynomial.monomial s) b = 0 ↔ b = 0
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>AddCommMonoid A<VAR>u : σ →₀ ℕ<VAR>r : R<VAR>b : (σ →₀ ℕ) → R → A<VAR>w : b u 0 = 0<GOAL>Finsupp.sum ((MvPolynomial.monomial u) r) b = b u r
<VAR>R : Type u<VAR>σ : Type u_1<VAR>a : R<VAR>CommSemiring R<VAR>A : Type u_2<VAR>AddCommMonoid A<VAR>b : (σ →₀ ℕ) → R → A<VAR>w : b 0 0 = 0<GOAL>Finsupp.sum (MvPolynomial.C a) b = b 0 a
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>α : Type u_2<VAR>s : Finset α<VAR>f : α → σ →₀ ℕ<GOAL>(MvPolynomial.monomial (∑ i ∈ s, f i)) 1 = ∏ i ∈ s, (MvPolynomial.monomial (f i)) 1
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>α : Type u_2<VAR>s : Finset α<VAR>f : α → σ →₀ ℕ<VAR>a : R<GOAL>(MvPolynomial.monomial (∑ i ∈ s, f i)) a = MvPolynomial.C a * ∏ i ∈ s, (MvPolynomial.monomial (f i)) 1
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Zero β<VAR>f : α →₀ β<VAR>g : α → β → σ →₀ ℕ<VAR>a : R<GOAL>(MvPolynomial.monomial (f.sum g)) a = MvPolynomial.C a * f.prod fun a b => (MvPolynomial.monomial (g a b)) 1
<VAR>R : Type u<VAR>CommSemiring R<VAR>α : Type u_2<VAR>a₁ a₂ : α →₀ ℕ<VAR>b₁ b₂ : R<GOAL>(MvPolynomial.monomial a₁) b₁ = (MvPolynomial.monomial a₂) b₂ ↔ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0
<VAR>R : Type u<VAR>σ : Type u_1<VAR>a : R<VAR>s : σ →₀ ℕ<VAR>CommSemiring R<GOAL>(MvPolynomial.monomial s) a = MvPolynomial.C a * s.prod fun n e => MvPolynomial.X n ^ e
<VAR>R : Type u<VAR>σ : Type u_1<VAR>s : σ →₀ ℕ<VAR>CommSemiring R<GOAL>∏ x ∈ s.support, MvPolynomial.X x ^ s x = (MvPolynomial.monomial s) 1
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>M : MvPolynomial σ R → Prop<VAR>h_C : ∀ (a : R), M (MvPolynomial.C a)<VAR>h_X : ∀ (p : MvPolynomial σ R) (n : σ), M p → M (p * MvPolynomial.X n)<VAR>s : σ →₀ ℕ<VAR>a : R<GOAL>M ((MvPolynomial.monomial s) a)
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>P : MvPolynomial σ R → Prop<VAR>p : MvPolynomial σ R<VAR>h1 : ∀ (u : σ →₀ ℕ) (a : R), P ((MvPolynomial.monomial u) a)<VAR>h2 : ∀ (p q : MvPolynomial σ R), P p → P q → P (p + q)<GOAL>P p
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>M : MvPolynomial σ R → Prop<VAR>p : MvPolynomial σ R<VAR>h_C : ∀ (a : R), M (MvPolynomial.C a)<VAR>h_add_weak : ∀ (a : σ →₀ ℕ) (b : R) (f : (σ →₀ ℕ) →₀ R), a ∉ f.support → b ≠ 0 → M f → M ((let_fun this := (MvPolynomial.monomial a) b; this) + f)<GOAL>M p
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>M : MvPolynomial σ R → Prop<VAR>p : MvPolynomial σ R<VAR>h_C : ∀ (a : R), M (MvPolynomial.C a)<VAR>h_add_weak : ∀ (a : σ →₀ ℕ) (b : R) (f : (σ →₀ ℕ) →₀ R), a ∉ f.support → b ≠ 0 → M f → M ((MvPolynomial.monomial a) b) → M ((let_fun this := (MvPolynomial.monomial a) b; this) + f)<VAR>h_X : ∀ (p : MvPolynomial σ R) (n : σ), M p → M (p * MvPolynomial.X n)<GOAL>M p
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>M : MvPolynomial σ R → Prop<VAR>p : MvPolynomial σ R<VAR>h_C : ∀ (a : R), M (MvPolynomial.C a)<VAR>h_add : ∀ (p q : MvPolynomial σ R), M p → M q → M (p + q)<VAR>h_X : ∀ (p : MvPolynomial σ R) (n : σ), M p → M (p * MvPolynomial.X n)<GOAL>M p
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>f g : MvPolynomial σ R →+* A<VAR>hC : ∀ (r : R), f (MvPolynomial.C r) = g (MvPolynomial.C r)<VAR>hX : ∀ (i : σ), f (MvPolynomial.X i) = g (MvPolynomial.X i)<GOAL>f = g
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>f g : MvPolynomial σ R →+* A<VAR>hC : f.comp MvPolynomial.C = g.comp MvPolynomial.C<VAR>hX : ∀ (i : σ), f (MvPolynomial.X i) = g (MvPolynomial.X i)<GOAL>f = g
<VAR>R : Type u<VAR>S₂ : Type w<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>Semiring S₂<VAR>f g : MvPolynomial σ R →+* S₂<VAR>hC : f.comp MvPolynomial.C = g.comp MvPolynomial.C<VAR>hX : ∀ (n : σ), f (MvPolynomial.X n) = g (MvPolynomial.X n)<VAR>p : MvPolynomial σ R<GOAL>f p = g p
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>f : MvPolynomial σ R →+* MvPolynomial σ R<VAR>hC : f.comp MvPolynomial.C = MvPolynomial.C<VAR>hX : ∀ (n : σ), f (MvPolynomial.X n) = MvPolynomial.X n<VAR>p : MvPolynomial σ R<GOAL>f p = p
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring A<VAR>CommSemiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>f g : MvPolynomial σ A →ₐ[R] B<VAR>h₁ : f.comp (IsScalarTower.toAlgHom R A (MvPolynomial σ A)) = g.comp (IsScalarTower.toAlgHom R A (MvPolynomial σ A))<VAR>h₂ : ∀ (i : σ), f (MvPolynomial.X i) = g (MvPolynomial.X i)<GOAL>f = g
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>Algebra R A<VAR>f g : MvPolynomial σ R →ₐ[R] A<VAR>hf : ∀ (i : σ), f (MvPolynomial.X i) = g (MvPolynomial.X i)<GOAL>f = g
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>Algebra R A<VAR>f : MvPolynomial σ R →ₐ[R] A<VAR>r : R<GOAL>f (MvPolynomial.C r) = (algebraMap R A) r
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<GOAL>Algebra.adjoin R (Set.range MvPolynomial.X) = ⊤
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>f g : MvPolynomial σ R →ₗ[R] M<VAR>h : ∀ (s : σ →₀ ℕ), f ∘ₗ MvPolynomial.monomial s = g ∘ₗ MvPolynomial.monomial s<GOAL>f = g
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>p : MvPolynomial σ R<GOAL>p.support = p.support
<VAR>R : Type u<VAR>σ : Type u_1<VAR>a : R<VAR>s : σ →₀ ℕ<VAR>CommSemiring R<VAR>h : Decidable (a = 0)<GOAL>((MvPolynomial.monomial s) a).support = if a = 0 then ∅ else {s}
<VAR>R : Type u<VAR>σ : Type u_1<VAR>a : R<VAR>s : σ →₀ ℕ<VAR>CommSemiring R<GOAL>((MvPolynomial.monomial s) a).support ⊆ {s}
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>DecidableEq σ<GOAL>(p + q).support ⊆ p.support ∪ q.support
<VAR>R : Type u<VAR>σ : Type u_1<VAR>n : σ<VAR>CommSemiring R<VAR>Nontrivial R<GOAL>(MvPolynomial.X n).support = {Finsupp.single n 1}
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>Nontrivial R<VAR>s : σ<VAR>n : ℕ<GOAL>(MvPolynomial.X s ^ n).support = {Finsupp.single s n}
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<GOAL>MvPolynomial.support 0 = ∅
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>S₁ : Type u_2<VAR>SMulZeroClass S₁ R<VAR>a : S₁<VAR>f : MvPolynomial σ R<GOAL>(a • f).support ⊆ f.support
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>α : Type u_2<VAR>DecidableEq σ<VAR>s : Finset α<VAR>f : α → MvPolynomial σ R<GOAL>(∑ x ∈ s, f x).support ⊆ s.biUnion fun x => (f x).support
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>p : MvPolynomial σ R<VAR>m : σ →₀ ℕ<GOAL>m ∈ p.support ↔ MvPolynomial.coeff m p ≠ 0
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>p : MvPolynomial σ R<VAR>m : σ →₀ ℕ<GOAL>m ∉ p.support ↔ MvPolynomial.coeff m p = 0
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>AddCommMonoid A<VAR>p : MvPolynomial σ R<VAR>b : (σ →₀ ℕ) → R → A<GOAL>Finsupp.sum p b = ∑ m ∈ p.support, b m (MvPolynomial.coeff m p)
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>DecidableEq σ<VAR>p q : MvPolynomial σ R<GOAL>(p * q).support ⊆ p.support + q.support
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>p q : MvPolynomial σ R<GOAL>(∀ (m : σ →₀ ℕ), MvPolynomial.coeff m p = MvPolynomial.coeff m q) → p = q
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>p q : MvPolynomial σ R<GOAL>p = q ↔ ∀ (m : σ →₀ ℕ), MvPolynomial.coeff m p = MvPolynomial.coeff m q
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>m : σ →₀ ℕ<VAR>p q : MvPolynomial σ R<GOAL>MvPolynomial.coeff m (p + q) = MvPolynomial.coeff m p + MvPolynomial.coeff m q
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>S₁ : Type u_2<VAR>SMulZeroClass S₁ R<VAR>m : σ →₀ ℕ<VAR>C : S₁<VAR>p : MvPolynomial σ R<GOAL>MvPolynomial.coeff m (C • p) = C • MvPolynomial.coeff m p
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>m : σ →₀ ℕ<GOAL>MvPolynomial.coeff m 0 = 0
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>i : σ<GOAL>MvPolynomial.coeff 0 (MvPolynomial.X i) = 0
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>m : σ →₀ ℕ<VAR>p : MvPolynomial σ R<GOAL>(MvPolynomial.coeffAddMonoidHom m) p = MvPolynomial.coeff m p
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>m : σ →₀ ℕ<VAR>p : MvPolynomial σ R<GOAL>(MvPolynomial.lcoeff R m) p = MvPolynomial.coeff m p
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>X : Type u_2<VAR>s : Finset X<VAR>f : X → MvPolynomial σ R<VAR>m : σ →₀ ℕ<GOAL>MvPolynomial.coeff m (∑ x ∈ s, f x) = ∑ x ∈ s, MvPolynomial.coeff m (f x)
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>m : σ →₀ ℕ<GOAL>(MvPolynomial.monomial m) 1 = m.prod fun n e => MvPolynomial.X n ^ e
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>DecidableEq σ<VAR>m n : σ →₀ ℕ<VAR>a : R<GOAL>MvPolynomial.coeff m ((MvPolynomial.monomial n) a) = if n = m then a else 0
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>DecidableEq σ<VAR>m : σ →₀ ℕ<VAR>a : R<GOAL>MvPolynomial.coeff m (MvPolynomial.C a) = if 0 = m then a else 0
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>IsEmpty σ<VAR>p : MvPolynomial σ R<GOAL>p = MvPolynomial.C (MvPolynomial.coeff 0 p)
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>DecidableEq σ<VAR>m : σ →₀ ℕ<GOAL>MvPolynomial.coeff m 1 = if 0 = m then 1 else 0
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>a : R<GOAL>MvPolynomial.coeff 0 (MvPolynomial.C a) = a
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<GOAL>MvPolynomial.coeff 0 1 = 1
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>DecidableEq σ<VAR>i : σ<VAR>m : σ →₀ ℕ<VAR>k : ℕ<GOAL>MvPolynomial.coeff m (MvPolynomial.X i ^ k) = if Finsupp.single i k = m then 1 else 0
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>DecidableEq σ<VAR>i : σ<VAR>m : σ →₀ ℕ<GOAL>MvPolynomial.coeff m (MvPolynomial.X i) = if Finsupp.single i 1 = m then 1 else 0
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>i : σ<GOAL>MvPolynomial.coeff (Finsupp.single i 1) (MvPolynomial.X i) = 1
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>m : σ →₀ ℕ<VAR>a : R<VAR>p : MvPolynomial σ R<GOAL>MvPolynomial.coeff m (MvPolynomial.C a * p) = a * MvPolynomial.coeff m p
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>DecidableEq σ<VAR>p q : MvPolynomial σ R<VAR>n : σ →₀ ℕ<GOAL>MvPolynomial.coeff n (p * q) = ∑ x ∈ Finset.antidiagonal n, MvPolynomial.coeff x.1 p * MvPolynomial.coeff x.2 q
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>m s : σ →₀ ℕ<VAR>r : R<VAR>p : MvPolynomial σ R<GOAL>MvPolynomial.coeff (m + s) (p * (MvPolynomial.monomial s) r) = MvPolynomial.coeff m p * r
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>m s : σ →₀ ℕ<VAR>r : R<VAR>p : MvPolynomial σ R<GOAL>MvPolynomial.coeff (s + m) ((MvPolynomial.monomial s) r * p) = r * MvPolynomial.coeff m p
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>m : σ →₀ ℕ<VAR>s : σ<VAR>p : MvPolynomial σ R<GOAL>MvPolynomial.coeff (m + Finsupp.single s 1) (p * MvPolynomial.X s) = MvPolynomial.coeff m p
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>m : σ →₀ ℕ<VAR>s : σ<VAR>p : MvPolynomial σ R<GOAL>MvPolynomial.coeff (Finsupp.single s 1 + m) (MvPolynomial.X s * p) = MvPolynomial.coeff m p
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>DecidableEq σ<VAR>s s' : σ<VAR>n n' : ℕ<GOAL>MvPolynomial.coeff (Finsupp.single s' n') (MvPolynomial.X s ^ n) = if s = s' ∧ n = n' ∨ n = 0 ∧ n' = 0 then 1 else 0
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>DecidableEq σ<VAR>s s' : σ<VAR>n : ℕ<GOAL>MvPolynomial.coeff (Finsupp.single s' n) (MvPolynomial.X s) = if n = 1 ∧ s = s' then 1 else 0
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>s : σ<VAR>p : MvPolynomial σ R<GOAL>(p * MvPolynomial.X s).support = Finset.map (addRightEmbedding (Finsupp.single s 1)) p.support
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>s : σ<VAR>p : MvPolynomial σ R<GOAL>(MvPolynomial.X s * p).support = Finset.map (addLeftEmbedding (Finsupp.single s 1)) p.support
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>S₁ : Type u_2<VAR>Semiring S₁<VAR>Module S₁ R<VAR>NoZeroSMulDivisors S₁ R<VAR>a : S₁<VAR>h : a ≠ 0<VAR>p : MvPolynomial σ R<GOAL>(a • p).support = p.support
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>DecidableEq σ<VAR>p q : MvPolynomial σ R<GOAL>p.support \ q.support ⊆ (p + q).support
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>DecidableEq σ<VAR>p q : MvPolynomial σ R<GOAL>symmDiff p.support q.support ⊆ (p + q).support
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>m s : σ →₀ ℕ<VAR>r : R<VAR>p : MvPolynomial σ R<GOAL>MvPolynomial.coeff m (p * (MvPolynomial.monomial s) r) = if s ≤ m then MvPolynomial.coeff (m - s) p * r else 0
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>m s : σ →₀ ℕ<VAR>r : R<VAR>p : MvPolynomial σ R<GOAL>MvPolynomial.coeff m ((MvPolynomial.monomial s) r * p) = if s ≤ m then r * MvPolynomial.coeff (m - s) p else 0
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>DecidableEq σ<VAR>m : σ →₀ ℕ<VAR>s : σ<VAR>p : MvPolynomial σ R<GOAL>MvPolynomial.coeff m (p * MvPolynomial.X s) = if s ∈ m.support then MvPolynomial.coeff (m - Finsupp.single s 1) p else 0
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>DecidableEq σ<VAR>m : σ →₀ ℕ<VAR>s : σ<VAR>p : MvPolynomial σ R<GOAL>MvPolynomial.coeff m (MvPolynomial.X s * p) = if s ∈ m.support then MvPolynomial.coeff (m - Finsupp.single s 1) p else 0
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>p : MvPolynomial σ R<GOAL>p = 0 ↔ ∀ (d : σ →₀ ℕ), MvPolynomial.coeff d p = 0
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>p : MvPolynomial σ R<GOAL>p ≠ 0 ↔ ∃ d, MvPolynomial.coeff d p ≠ 0
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>Nontrivial R<VAR>s : σ<GOAL>MvPolynomial.X s ≠ 0
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>p : MvPolynomial σ R<GOAL>p.support = ∅ ↔ p = 0
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>p : MvPolynomial σ R<GOAL>p.support.Nonempty ↔ p ≠ 0
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>p : MvPolynomial σ R<VAR>h : p ≠ 0<GOAL>∃ d, MvPolynomial.coeff d p ≠ 0
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>r : R<VAR>φ : MvPolynomial σ R<GOAL>MvPolynomial.C r ∣ φ ↔ ∀ (i : σ →₀ ℕ), r ∣ MvPolynomial.coeff i φ
<VAR>R : Type u<VAR>σ : Type u_1<VAR>n : σ<VAR>CommSemiring R<GOAL>IsRegular (MvPolynomial.X n)
<VAR>R : Type u<VAR>σ : Type u_1<VAR>n : σ<VAR>CommSemiring R<VAR>k : ℕ<GOAL>IsRegular (MvPolynomial.X n ^ k)
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>s : Finset σ<GOAL>IsRegular (∏ n ∈ s, MvPolynomial.X n)
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<GOAL>MvPolynomial.coeffs 0 = ∅
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<GOAL>MvPolynomial.coeffs 1 ⊆ {1}
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>Subsingleton R<VAR>p : MvPolynomial σ R<GOAL>p.coeffs = ∅
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>Nontrivial R<GOAL>MvPolynomial.coeffs 1 = {1}
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>p : MvPolynomial σ R<VAR>c : R<GOAL>c ∈ p.coeffs ↔ ∃ n ∈ p.support, c = MvPolynomial.coeff n p