ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>SubtractionCommMonoid α<VAR>m : Multiset ι<VAR>f : ι → α<VAR>n : ℤ<GOAL>(Multiset.map (fun i => n • f i) m).sum = n • (Multiset.map f m).sum
<VAR>α : Type u_3<VAR>s : Multiset α<GOAL>(Multiset.map (fun a => {a}) s).sum = s
<VAR>s : Multiset ℕ<VAR>n : ℕ<GOAL>s.sum % n = (Multiset.map (fun x => x % n) s).sum % n
<VAR>s : Multiset ℕ<VAR>n : ℕ<GOAL>s.prod % n = (Multiset.map (fun x => x % n) s).prod % n
<VAR>s : Multiset ℤ<VAR>n : ℤ<GOAL>s.sum % n = (Multiset.map (fun x => x % n) s).sum % n
<VAR>s : Multiset ℤ<VAR>n : ℤ<GOAL>s.prod % n = (Multiset.map (fun x => x % n) s).prod % n
<VAR>α : Type u_6<VAR>NonUnitalNonAssocSemiring α<VAR>self : CentroidHom α<VAR>a b : α<GOAL>(↑self.toAddMonoidHom).toFun (a * b) = (↑self.toAddMonoidHom).toFun a * b
<VAR>α : Type u_6<VAR>NonUnitalNonAssocSemiring α<VAR>self : CentroidHom α<VAR>a b : α<GOAL>(↑self.toAddMonoidHom).toFun (a * b) = a * (↑self.toAddMonoidHom).toFun b
<VAR>F : Type u_6<VAR>α : Type u_7<VAR>NonUnitalNonAssocSemiring α<VAR>FunLike F α α<VAR>self : CentroidHomClass F α<VAR>f : F<VAR>a b : α<GOAL>f (a * b) = f a * b
<VAR>F : Type u_6<VAR>α : Type u_7<VAR>NonUnitalNonAssocSemiring α<VAR>FunLike F α α<VAR>self : CentroidHomClass F α<VAR>f : F<VAR>a b : α<GOAL>f (a * b) = a * f b
<VAR>α : Type u_5<VAR>NonUnitalNonAssocSemiring α<VAR>f : CentroidHom α<GOAL>(↑f.toAddMonoidHom).toFun = ⇑f
<VAR>α : Type u_5<VAR>NonUnitalNonAssocSemiring α<VAR>f g : CentroidHom α<VAR>h : ∀ (a : α), f a = g a<GOAL>f = g
<VAR>α : Type u_5<VAR>NonUnitalNonAssocSemiring α<VAR>f : CentroidHom α<GOAL>⇑↑f = ⇑f
<VAR>α : Type u_5<VAR>NonUnitalNonAssocSemiring α<VAR>f : CentroidHom α<GOAL>f.toAddMonoidHom = ↑f
<VAR>α : Type u_5<VAR>NonUnitalNonAssocSemiring α<GOAL>Function.Injective AddMonoidHomClass.toAddMonoidHom
<VAR>α : Type u_5<VAR>NonUnitalNonAssocSemiring α<GOAL>Function.Injective CentroidHom.toEnd
<VAR>α : Type u_5<VAR>NonUnitalNonAssocSemiring α<VAR>f : CentroidHom α<VAR>f' : α → α<VAR>h : f' = ⇑f<GOAL>⇑(f.copy f' h) = f'
<VAR>α : Type u_5<VAR>NonUnitalNonAssocSemiring α<VAR>f : CentroidHom α<VAR>f' : α → α<VAR>h : f' = ⇑f<GOAL>f.copy f' h = f
<VAR>α : Type u_5<VAR>NonUnitalNonAssocSemiring α<GOAL>⇑(CentroidHom.id α) = id
<VAR>α : Type u_5<VAR>NonUnitalNonAssocSemiring α<GOAL>↑(CentroidHom.id α) = AddMonoidHom.id α
<VAR>α : Type u_5<VAR>NonUnitalNonAssocSemiring α<VAR>a : α<GOAL>(CentroidHom.id α) a = a
<VAR>α : Type u_5<VAR>NonUnitalNonAssocSemiring α<VAR>g f : CentroidHom α<GOAL>⇑(g.comp f) = ⇑g ∘ ⇑f
<VAR>α : Type u_5<VAR>NonUnitalNonAssocSemiring α<VAR>g f : CentroidHom α<VAR>a : α<GOAL>(g.comp f) a = g (f a)
<VAR>α : Type u_5<VAR>NonUnitalNonAssocSemiring α<VAR>g f : CentroidHom α<GOAL>↑(g.comp f) = (↑g).comp ↑f
<VAR>α : Type u_5<VAR>NonUnitalNonAssocSemiring α<VAR>h g f : CentroidHom α<GOAL>(h.comp g).comp f = h.comp (g.comp f)
<VAR>α : Type u_5<VAR>NonUnitalNonAssocSemiring α<VAR>f : CentroidHom α<GOAL>f.comp (CentroidHom.id α) = f
<VAR>α : Type u_5<VAR>NonUnitalNonAssocSemiring α<VAR>f : CentroidHom α<GOAL>(CentroidHom.id α).comp f = f
<VAR>α : Type u_5<VAR>NonUnitalNonAssocSemiring α<VAR>g₁ g₂ f : CentroidHom α<VAR>hf : Function.Surjective ⇑f<GOAL>g₁.comp f = g₂.comp f ↔ g₁ = g₂
<VAR>α : Type u_5<VAR>NonUnitalNonAssocSemiring α<VAR>g f₁ f₂ : CentroidHom α<VAR>hg : Function.Injective ⇑g<GOAL>g.comp f₁ = g.comp f₂ ↔ f₁ = f₂
<VAR>α : Type u_5<VAR>NonUnitalNonAssocSemiring α<GOAL>⇑0 = 0
<VAR>α : Type u_5<VAR>NonUnitalNonAssocSemiring α<GOAL>⇑1 = id
<VAR>α : Type u_5<VAR>NonUnitalNonAssocSemiring α<VAR>f g : CentroidHom α<GOAL>⇑(f + g) = ⇑f + ⇑g
<VAR>α : Type u_5<VAR>NonUnitalNonAssocSemiring α<VAR>f g : CentroidHom α<GOAL>⇑(f * g) = ⇑f ∘ ⇑g
<VAR>M : Type u_2<VAR>α : Type u_5<VAR>NonUnitalNonAssocSemiring α<VAR>Monoid M<VAR>DistribMulAction M α<VAR>SMulCommClass M α α<VAR>IsScalarTower M α α<VAR>n : M<VAR>f : CentroidHom α<GOAL>⇑(n • f) = n • ⇑f
<VAR>α : Type u_5<VAR>NonUnitalNonAssocSemiring α<VAR>a : α<GOAL>0 a = 0
<VAR>α : Type u_5<VAR>NonUnitalNonAssocSemiring α<VAR>a : α<GOAL>1 a = a
<VAR>α : Type u_5<VAR>NonUnitalNonAssocSemiring α<VAR>f g : CentroidHom α<VAR>a : α<GOAL>(f + g) a = f a + g a
<VAR>α : Type u_5<VAR>NonUnitalNonAssocSemiring α<VAR>f g : CentroidHom α<VAR>a : α<GOAL>(f * g) a = f (g a)
<VAR>M : Type u_2<VAR>α : Type u_5<VAR>NonUnitalNonAssocSemiring α<VAR>Monoid M<VAR>DistribMulAction M α<VAR>SMulCommClass M α α<VAR>IsScalarTower M α α<VAR>n : M<VAR>f : CentroidHom α<VAR>a : α<GOAL>(n • f) a = n • f a
<VAR>α : Type u_5<VAR>NonUnitalNonAssocSemiring α<GOAL>CentroidHom.toEnd 0 = 0
<VAR>α : Type u_5<VAR>NonUnitalNonAssocSemiring α<VAR>x y : CentroidHom α<GOAL>(x + y).toEnd = x.toEnd + y.toEnd
<VAR>M : Type u_2<VAR>α : Type u_5<VAR>NonUnitalNonAssocSemiring α<VAR>Monoid M<VAR>DistribMulAction M α<VAR>SMulCommClass M α α<VAR>IsScalarTower M α α<VAR>m : M<VAR>x : CentroidHom α<GOAL>(m • x).toEnd = m • x.toEnd
<VAR>α : Type u_5<VAR>NonUnitalNonAssocSemiring α<VAR>n : ℕ<GOAL>⇑↑n = n • ⇑(CentroidHom.id α)
<VAR>α : Type u_5<VAR>NonUnitalNonAssocSemiring α<VAR>n : ℕ<VAR>m : α<GOAL>↑n m = n • m
<VAR>α : Type u_5<VAR>NonUnitalNonAssocSemiring α<GOAL>CentroidHom.toEnd 1 = 1
<VAR>α : Type u_5<VAR>NonUnitalNonAssocSemiring α<VAR>x y : CentroidHom α<GOAL>(x * y).toEnd = x.toEnd * y.toEnd
<VAR>α : Type u_5<VAR>NonUnitalNonAssocSemiring α<VAR>x : CentroidHom α<VAR>n : ℕ<GOAL>(x ^ n).toEnd = x.toEnd ^ n
<VAR>α : Type u_5<VAR>NonUnitalNonAssocSemiring α<VAR>n : ℕ<GOAL>(↑n).toEnd = ↑n
<VAR>α : Type u_5<VAR>NonUnitalNonAssocSemiring α<VAR>f : CentroidHom α<GOAL>(CentroidHom.toEndRingHom α) f = f.toEnd
<VAR>α : Type u_5<VAR>NonUnitalNonAssocSemiring α<VAR>T S : CentroidHom α<VAR>a b : α<GOAL>(⇑T ∘ ⇑S) (a * b) = (⇑S ∘ ⇑T) (a * b)
<VAR>α : Type u_5<VAR>NonUnitalNonAssocSemiring α<VAR>T : CentroidHom α<VAR>a : α<GOAL>T • a = T a
<VAR>α : Type u_5<VAR>NonUnitalNonAssocSemiring α<VAR>R : Type u_6<VAR>CommSemiring R<VAR>Module R α<VAR>SMulCommClass R α α<VAR>IsScalarTower R α α<VAR>x : R<VAR>a : α<GOAL>(Module.toCentroidHom x) a = x • a
<VAR>α : Type u_5<VAR>NonUnitalNonAssocSemiring α<GOAL>(CentroidHom.toEndRingHom α).rangeS = Subsemiring.centralizer (Set.range ⇑AddMonoid.End.mulLeft ∪ Set.range ⇑AddMonoid.End.mulRight)
<VAR>α : Type u_5<VAR>NonUnitalNonAssocSemiring α<VAR>z : ↥(NonUnitalSubsemiring.center α)<VAR>a : α<GOAL>(CentroidHom.centerToCentroidCenter z) a = ↑z * a
<VAR>α : Type u_5<VAR>NonUnitalNonAssocSemiring α<VAR>z : ↥(NonUnitalSubsemiring.center α)<VAR>a : α<GOAL>(CentroidHom.centerToCentroid z) a = ↑z * a
<VAR>α : Type u_5<VAR>NonUnitalNonAssocSemiring α<VAR>a : α<GOAL>a ∈ NonUnitalSubsemiring.center α ↔ AddMonoid.End.mulRight a = AddMonoid.End.mulLeft a ∧ AddMonoid.End.mulLeft a ∈ (CentroidHom.toEndRingHom α).rangeS
<VAR>α : Type u_5<VAR>NonUnitalNonAssocCommSemiring α<VAR>a : α<GOAL>a ∈ NonUnitalSubsemiring.center α ↔ ∀ (b : α), Commute (AddMonoid.End.mulLeft b) (AddMonoid.End.mulLeft a)
<VAR>α : Type u_5<VAR>NonUnitalNonAssocRing α<VAR>z : ℤ<GOAL>⇑↑z = z • ⇑(CentroidHom.id α)
<VAR>α : Type u_5<VAR>NonUnitalNonAssocRing α<VAR>z : ℤ<VAR>m : α<GOAL>↑z m = z • m
<VAR>α : Type u_5<VAR>NonUnitalNonAssocRing α<VAR>x : CentroidHom α<GOAL>(-x).toEnd = -x.toEnd
<VAR>α : Type u_5<VAR>NonUnitalNonAssocRing α<VAR>x y : CentroidHom α<GOAL>(x - y).toEnd = x.toEnd - y.toEnd
<VAR>α : Type u_5<VAR>NonUnitalNonAssocRing α<VAR>f : CentroidHom α<GOAL>⇑(-f) = -⇑f
<VAR>α : Type u_5<VAR>NonUnitalNonAssocRing α<VAR>f g : CentroidHom α<GOAL>⇑(f - g) = ⇑f - ⇑g
<VAR>α : Type u_5<VAR>NonUnitalNonAssocRing α<VAR>f : CentroidHom α<VAR>a : α<GOAL>(-f) a = -f a
<VAR>α : Type u_5<VAR>NonUnitalNonAssocRing α<VAR>f g : CentroidHom α<VAR>a : α<GOAL>(f - g) a = f a - g a
<VAR>α : Type u_5<VAR>NonUnitalNonAssocRing α<VAR>z : ℤ<GOAL>(↑z).toEnd = ↑z
<VAR>M : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<GOAL>AddMonoidAlgebra.gradeBy R id = AddMonoidAlgebra.grade R
<VAR>M : Type u_1<VAR>ι : Type u_2<VAR>R : Type u_3<VAR>CommSemiring R<VAR>f : M → ι<VAR>i : ι<VAR>a : AddMonoidAlgebra R M<GOAL>a ∈ AddMonoidAlgebra.gradeBy R f i ↔ ↑a.support ⊆ f ⁻¹' {i}
<VAR>M : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<VAR>m : M<VAR>a : AddMonoidAlgebra R M<GOAL>a ∈ AddMonoidAlgebra.grade R m ↔ a.support ⊆ {m}
<VAR>M : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<VAR>m : M<VAR>a : AddMonoidAlgebra R M<GOAL>a ∈ AddMonoidAlgebra.grade R m ↔ a ∈ LinearMap.range (Finsupp.lsingle m)
<VAR>M : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<VAR>m : M<GOAL>AddMonoidAlgebra.grade R m = LinearMap.range (Finsupp.lsingle m)
<VAR>M : Type u_1<VAR>ι : Type u_2<VAR>R : Type u_4<VAR>CommSemiring R<VAR>f : M → ι<VAR>m : M<VAR>r : R<GOAL>Finsupp.single m r ∈ AddMonoidAlgebra.gradeBy R f (f m)
<VAR>M : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>i : M<VAR>r : R<GOAL>Finsupp.single i r ∈ AddMonoidAlgebra.grade R i
<VAR>M : Type u_1<VAR>ι : Type u_2<VAR>R : Type u_3<VAR>AddMonoid M<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>CommSemiring R<VAR>f : M →+ ι<VAR>m : M<VAR>r : R<GOAL>(AddMonoidAlgebra.decomposeAux f) (Finsupp.single m r) = (DirectSum.of (fun i => ↥(AddMonoidAlgebra.gradeBy R (⇑f) i)) (f m)) ⟨Finsupp.single m r, ⋯⟩
<VAR>M : Type u_1<VAR>ι : Type u_2<VAR>R : Type u_3<VAR>AddMonoid M<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>CommSemiring R<VAR>f : M →+ ι<VAR>i : ι<VAR>x : ↥(AddMonoidAlgebra.gradeBy R (⇑f) i)<GOAL>(AddMonoidAlgebra.decomposeAux f) ↑x = (DirectSum.of (fun i => ↥(AddMonoidAlgebra.gradeBy R (⇑f) i)) i) x
<VAR>M : Type u_1<VAR>ι : Type u_2<VAR>R : Type u_3<VAR>AddMonoid M<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>CommSemiring R<VAR>f : M →+ ι<GOAL>⇑(AddMonoidAlgebra.decomposeAux f) = ⇑(DirectSum.decompose (AddMonoidAlgebra.gradeBy R ⇑f))
<VAR>M : Type u_1<VAR>ι : Type u_2<VAR>R : Type u_3<VAR>AddMonoid M<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>CommSemiring R<VAR>f : M →+ ι<VAR>m : M<VAR>r : R<GOAL>(DirectSum.decompose (AddMonoidAlgebra.gradeBy R ⇑f)) (Finsupp.single m r) = (DirectSum.of (fun i => ↥(AddMonoidAlgebra.gradeBy R (⇑f) i)) (f m)) ⟨Finsupp.single m r, ⋯⟩
<VAR>ι : Type u_2<VAR>R : Type u_3<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>CommSemiring R<VAR>i : ι<VAR>r : R<GOAL>(DirectSum.decompose (AddMonoidAlgebra.grade R)) (Finsupp.single i r) = (DirectSum.of (fun i => ↥(AddMonoidAlgebra.grade R i)) i) ⟨Finsupp.single i r, ⋯⟩
<VAR>M : Type u_1<VAR>ι : Type u_2<VAR>R : Type u_3<VAR>AddMonoid M<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>CommSemiring R<VAR>f : M →+ ι<GOAL>DirectSum.IsInternal (AddMonoidAlgebra.gradeBy R ⇑f)
<VAR>ι : Type u_2<VAR>R : Type u_3<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>CommSemiring R<GOAL>DirectSum.IsInternal (AddMonoidAlgebra.grade R)
<VAR>R : Type u<VAR>CommRing R<VAR>p : ℕ<VAR>hp1 : Fact (Nat.Prime p)<VAR>hp2 : ↑p ∈ nonunits R<GOAL>CharP (R ⧸ Ideal.span {↑p}) p
<VAR>R : Type u_1<VAR>CommRing R<VAR>p : ℕ<VAR>CharP R p<VAR>I : Ideal R<VAR>h : ∀ (x : ℕ), ↑x ∈ I → ↑x = 0<GOAL>CharP (R ⧸ I) p
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℕ<VAR>CharP R n<VAR>I : Ideal R<GOAL>CharP (R ⧸ I) n ↔ ∀ (x : ℕ), ↑x ∈ I → ↑x = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℕ<VAR>CharP R n<VAR>I : Ideal R<GOAL>CharP (R ⧸ I) n ↔ Ideal.comap (Nat.castRingHom R) I ≤ RingHom.ker (Nat.castRingHom R)
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<GOAL>↑(Submodule.toAddSubgroup I).index = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsReduced R<VAR>p n : ℕ<VAR>ExpChar R p<GOAL>Function.Injective ⇑(iterateFrobenius R p n)
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsReduced R<VAR>p : ℕ<VAR>ExpChar R p<GOAL>Function.Injective ⇑(frobenius R p)
<VAR>R : Type u_1<VAR>Finite R<VAR>CommRing R<VAR>IsReduced R<VAR>CharP R 2<VAR>a : R<GOAL>IsSquare a
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsReduced R<VAR>p k m : ℕ<VAR>ExpChar R p<VAR>x : R<GOAL>x ^ (p ^ k * m) = 1 ↔ x ^ m = 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>LocalRing R<VAR>q : ℕ<VAR>char_R_q : CharP R q<GOAL>q = 0 ∨ IsPrimePow q
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>X : Type u_2<VAR>x y : FreeAlgebra.Pre R X<GOAL>Quot.mk (FreeAlgebra.Rel R X) (x * y) = Quot.mk (FreeAlgebra.Rel R X) x * Quot.mk (FreeAlgebra.Rel R X) y
<VAR>R : Type u_3<VAR>CommSemiring R<VAR>X : Type u_4<VAR>m : X<GOAL>FreeAlgebra.ι R m = Quot.mk (FreeAlgebra.Rel R X) (FreeAlgebra.Pre.of m)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>X : Type u_2<VAR>m : X<GOAL>Quot.mk (FreeAlgebra.Rel R X) (FreeAlgebra.Pre.of m) = FreeAlgebra.ι R m
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>X : Type u_2<VAR>A : Type u_3<VAR>Semiring A<VAR>Algebra R A<VAR>f : X → A<GOAL>FreeAlgebra.liftAux R f = (FreeAlgebra.lift R) f
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>X : Type u_2<VAR>A : Type u_3<VAR>Semiring A<VAR>Algebra R A<VAR>F : FreeAlgebra R X →ₐ[R] A<GOAL>(FreeAlgebra.lift R).symm F = ⇑F ∘ FreeAlgebra.ι R
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>X : Type u_2<VAR>A : Type u_3<VAR>Semiring A<VAR>Algebra R A<VAR>f : X → A<GOAL>⇑((FreeAlgebra.lift R) f) ∘ FreeAlgebra.ι R = f
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>X : Type u_2<VAR>A : Type u_3<VAR>Semiring A<VAR>Algebra R A<VAR>f : X → A<VAR>x : X<GOAL>((FreeAlgebra.lift R) f) (FreeAlgebra.ι R x) = f x
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>X : Type u_2<VAR>A : Type u_3<VAR>Semiring A<VAR>Algebra R A<VAR>f : X → A<VAR>g : FreeAlgebra R X →ₐ[R] A<GOAL>⇑g ∘ FreeAlgebra.ι R = f ↔ g = (FreeAlgebra.lift R) f
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>X : Type u_2<VAR>A : Type u_3<VAR>Semiring A<VAR>Algebra R A<VAR>g : FreeAlgebra R X →ₐ[R] A<GOAL>(FreeAlgebra.lift R) (⇑g ∘ FreeAlgebra.ι R) = g
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>X : Type u_2<VAR>A : Type u_3<VAR>Semiring A<VAR>Algebra R A<VAR>f g : FreeAlgebra R X →ₐ[R] A<VAR>w : ⇑f ∘ FreeAlgebra.ι R = ⇑g ∘ FreeAlgebra.ι R<GOAL>f = g
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>X : Type u_2<GOAL>Function.LeftInverse ⇑FreeAlgebra.algebraMapInv ⇑(algebraMap R (FreeAlgebra R X))
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>X : Type u_2<VAR>x y : R<GOAL>(algebraMap R (FreeAlgebra R X)) x = (algebraMap R (FreeAlgebra R X)) y ↔ x = y
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>X : Type u_2<VAR>x : R<GOAL>(algebraMap R (FreeAlgebra R X)) x = 0 ↔ x = 0
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>X : Type u_2<VAR>x : R<GOAL>(algebraMap R (FreeAlgebra R X)) x = 1 ↔ x = 1
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>X : Type u_2<VAR>Nontrivial R<GOAL>Function.Injective (FreeAlgebra.ι R)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>X : Type u_2<VAR>Nontrivial R<VAR>x y : X<GOAL>FreeAlgebra.ι R x = FreeAlgebra.ι R y ↔ x = y
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>X : Type u_2<VAR>Nontrivial R<VAR>x : X<VAR>r : R<GOAL>FreeAlgebra.ι R x ≠ (algebraMap R (FreeAlgebra R X)) r
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>X : Type u_2<VAR>Nontrivial R<VAR>x : X<GOAL>FreeAlgebra.ι R x ≠ 0
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>X : Type u_2<VAR>Nontrivial R<VAR>x : X<GOAL>FreeAlgebra.ι R x ≠ 1
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>X : Type u_2<VAR>C : FreeAlgebra R X → Prop<VAR>h_grade0 : ∀ (r : R), C ((algebraMap R (FreeAlgebra R X)) r)<VAR>h_grade1 : ∀ (x : X), C (FreeAlgebra.ι R x)<VAR>h_mul : ∀ (a b : FreeAlgebra R X), C a → C b → C (a * b)<VAR>h_add : ∀ (a b : FreeAlgebra R X), C a → C b → C (a + b)<VAR>a : FreeAlgebra R X<GOAL>C a
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>X : Type u_2<GOAL>Algebra.adjoin R (Set.range (FreeAlgebra.ι R)) = ⊤
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>X : Type u_2<VAR>A : Type u_3<VAR>Semiring A<VAR>Algebra R A<VAR>f : X → A<GOAL>Algebra.adjoin R (Set.range f) = ((FreeAlgebra.lift R) f).range
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_3<VAR>Semiring A<VAR>Algebra R A<VAR>s : Set A<GOAL>Algebra.adjoin R s = ((FreeAlgebra.lift R) Subtype.val).range
<VAR>R : Type u_1<VAR>Semiring R<VAR>CharP R 2<GOAL>2 = 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>CharP R 2<VAR>x : R<GOAL>x + x = 0
<VAR>R : Type u_1<VAR>Ring R<VAR>CharP R 2<VAR>x : R<GOAL>-x = x
<VAR>R : Type u_1<VAR>Ring R<VAR>CharP R 2<GOAL>Neg.neg = id
<VAR>R : Type u_1<VAR>Ring R<VAR>CharP R 2<VAR>x y : R<GOAL>x - y = x + y
<VAR>R : Type u_1<VAR>Ring R<VAR>CharP R 2<GOAL>HSub.hSub = fun x x_1 => x + x_1
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>CharP R 2<VAR>x y : R<GOAL>(x + y) ^ 2 = x ^ 2 + y ^ 2
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>CharP R 2<VAR>x y : R<GOAL>(x + y) * (x + y) = x * x + y * y
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>CharP R 2<VAR>l : List R<GOAL>l.sum ^ 2 = (List.map (fun x => x ^ 2) l).sum
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>CharP R 2<VAR>l : List R<GOAL>l.sum * l.sum = (List.map (fun x => x * x) l).sum
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>CharP R 2<VAR>l : Multiset R<GOAL>l.sum ^ 2 = (Multiset.map (fun x => x ^ 2) l).sum
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>CharP R 2<VAR>l : Multiset R<GOAL>l.sum * l.sum = (Multiset.map (fun x => x * x) l).sum
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>CommSemiring R<VAR>CharP R 2<VAR>s : Finset ι<VAR>f : ι → R<GOAL>(∑ i ∈ s, f i) ^ 2 = ∑ i ∈ s, f i ^ 2
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>CommSemiring R<VAR>CharP R 2<VAR>s : Finset ι<VAR>f : ι → R<GOAL>(∑ i ∈ s, f i) * ∑ i ∈ s, f i = ∑ i ∈ s, f i * f i
<VAR>R : Type u_1<VAR>Ring R<VAR>Nontrivial R<GOAL>-1 = 1 ↔ ringChar R = 2
<VAR>R : Type u_1<VAR>Ring R<VAR>Nontrivial R<GOAL>orderOf (-1) = if ringChar R = 2 then 1 else 2
<VAR>R : Type u_1<VAR>Semiring R<VAR>p : ℕ<VAR>x y : R<VAR>hp : Nat.Prime p<VAR>h : Commute x y<VAR>n : ℕ<GOAL>(x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + ↑p * ∑ k ∈ Finset.Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k / p)
<VAR>R : Type u_1<VAR>Semiring R<VAR>p : ℕ<VAR>x y : R<VAR>hp : Nat.Prime p<VAR>h : Commute x y<GOAL>(x + y) ^ p = x ^ p + y ^ p + ↑p * ∑ k ∈ Finset.Ioo 0 p, x ^ k * y ^ (p - k) * ↑(p.choose k / p)
<VAR>R : Type u_1<VAR>Semiring R<VAR>p : ℕ<VAR>x y : R<VAR>hp : Nat.Prime p<VAR>h : Commute x y<VAR>n : ℕ<GOAL>∃ r, (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + ↑p * r
<VAR>R : Type u_1<VAR>Semiring R<VAR>p : ℕ<VAR>x y : R<VAR>hp : Nat.Prime p<VAR>h : Commute x y<GOAL>∃ r, (x + y) ^ p = x ^ p + y ^ p + ↑p * r
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>x y : R<VAR>n : ℕ<GOAL>(x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + ↑p * ∑ k ∈ Finset.Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k / p)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>x y : R<GOAL>(x + y) ^ p = x ^ p + y ^ p + ↑p * ∑ k ∈ Finset.Ioo 0 p, x ^ k * y ^ (p - k) * ↑(p.choose k / p)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>x y : R<VAR>n : ℕ<GOAL>∃ r, (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + ↑p * r
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>x y : R<GOAL>∃ r, (x + y) ^ p = x ^ p + y ^ p + ↑p * r
<VAR>R : Type u_1<VAR>Semiring R<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>CharP R p<VAR>x y : R<VAR>h : Commute x y<GOAL>(x + y) ^ p = x ^ p + y ^ p
<VAR>R : Type u_1<VAR>Semiring R<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>CharP R p<VAR>x y : R<VAR>h : Commute x y<GOAL>(x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n
<VAR>R : Type u_1<VAR>Ring R<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>CharP R p<VAR>x y : R<VAR>h : Commute x y<GOAL>(x - y) ^ p = x ^ p - y ^ p
<VAR>R : Type u_1<VAR>Ring R<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>CharP R p<VAR>n : ℕ<VAR>x y : R<VAR>h : Commute x y<GOAL>(x - y) ^ p ^ n = x ^ p ^ n - y ^ p ^ n
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>CharP R p<VAR>x y : R<GOAL>(x + y) ^ p = x ^ p + y ^ p
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>CharP R p<VAR>n : ℕ<VAR>x y : R<GOAL>(x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>CharP R p<VAR>n : ℕ<VAR>x y : R<GOAL>(x + y) ^ n = (x + y) ^ (n % p) * (x ^ p + y ^ p) ^ (n / p)
<VAR>R : Type u_1<VAR>CommRing R<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>CharP R p<VAR>x y : R<GOAL>(x - y) ^ p = x ^ p - y ^ p
<VAR>R : Type u_1<VAR>CommRing R<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>CharP R p<VAR>n : ℕ<VAR>x y : R<GOAL>(x - y) ^ p ^ n = x ^ p ^ n - y ^ p ^ n
<VAR>R : Type u_1<VAR>CommRing R<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>CharP R p<VAR>n : ℕ<VAR>x y : R<GOAL>(x - y) ^ n = (x - y) ^ (n % p) * (x ^ p - y ^ p) ^ (n / p)
<VAR>R : Type u_1<VAR>Ring R<VAR>p : ℕ<VAR>CharP R p<VAR>Fact (Nat.Prime p)<GOAL>(-1) ^ p = -1
<VAR>R : Type u_1<VAR>Ring R<VAR>p n : ℕ<VAR>CharP R p<VAR>Fact (Nat.Prime p)<GOAL>(-1) ^ p ^ n = -1
<VAR>R : Type u_1<VAR>NonAssocRing R<VAR>p : ℕ<VAR>CharP R p<VAR>Finite R<GOAL>p ≠ 0
<VAR>R : Type u_1<VAR>NonAssocRing R<VAR>Finite R<GOAL>ringChar R ≠ 0
<VAR>R : Type u_1<VAR>Ring R<VAR>NoZeroDivisors R<VAR>Nontrivial R<VAR>Finite R<VAR>p : ℕ<VAR>CharP R p<GOAL>Nat.Prime p
<VAR>K : Type u_1<VAR>Field K<VAR>t : ℕ<VAR>Invertible ↑t<GOAL>¬ringChar K ∣ t
<VAR>β : Type u_2<VAR>CommMonoid β<VAR>n : ℕ<VAR>f : ℕ → β<GOAL>∏ i ∈ Finset.range n, f i = ∏ i : Fin n, f ↑i
<VAR>β : Type u_2<VAR>AddCommMonoid β<VAR>n : ℕ<VAR>f : ℕ → β<GOAL>∑ i ∈ Finset.range n, f i = ∑ i : Fin n, f ↑i
<VAR>β : Type u_2<VAR>CommMonoid β<VAR>n : ℕ<VAR>f : Fin n → β<GOAL>(List.ofFn f).prod = ∏ i : Fin n, f i
<VAR>β : Type u_2<VAR>AddCommMonoid β<VAR>n : ℕ<VAR>f : Fin n → β<GOAL>(List.ofFn f).sum = ∑ i : Fin n, f i
<VAR>β : Type u_2<VAR>AddCommMonoid β<VAR>n : ℕ<VAR>f : Fin n → β<GOAL>∑ i : Fin n, f i = (List.map f (List.finRange n)).sum
<VAR>β : Type u_2<VAR>CommMonoid β<VAR>n : ℕ<VAR>f : Fin n → β<GOAL>∏ i : Fin n, f i = (List.map f (List.finRange n)).prod
<VAR>β : Type u_2<VAR>CommMonoid β<VAR>f : Fin 0 → β<GOAL>∏ i : Fin 0, f i = 1
<VAR>β : Type u_2<VAR>AddCommMonoid β<VAR>f : Fin 0 → β<GOAL>∑ i : Fin 0, f i = 0
<VAR>β : Type u_2<VAR>CommMonoid β<VAR>n : ℕ<VAR>f : Fin (n + 1) → β<VAR>x : Fin (n + 1)<GOAL>∏ i : Fin (n + 1), f i = f x * ∏ i : Fin n, f (x.succAbove i)
<VAR>β : Type u_2<VAR>AddCommMonoid β<VAR>n : ℕ<VAR>f : Fin (n + 1) → β<VAR>x : Fin (n + 1)<GOAL>∑ i : Fin (n + 1), f i = f x + ∑ i : Fin n, f (x.succAbove i)
<VAR>β : Type u_2<VAR>CommMonoid β<VAR>n : ℕ<VAR>f : Fin (n + 1) → β<GOAL>∏ i : Fin (n + 1), f i = f 0 * ∏ i : Fin n, f i.succ
<VAR>β : Type u_2<VAR>AddCommMonoid β<VAR>n : ℕ<VAR>f : Fin (n + 1) → β<GOAL>∑ i : Fin (n + 1), f i = f 0 + ∑ i : Fin n, f i.succ
<VAR>β : Type u_2<VAR>CommMonoid β<VAR>n : ℕ<VAR>f : Fin (n + 1) → β<GOAL>∏ i : Fin (n + 1), f i = (∏ i : Fin n, f i.castSucc) * f (Fin.last n)
<VAR>β : Type u_2<VAR>AddCommMonoid β<VAR>n : ℕ<VAR>f : Fin (n + 1) → β<GOAL>∑ i : Fin (n + 1), f i = ∑ i : Fin n, f i.castSucc + f (Fin.last n)
<VAR>α : Type u_1<VAR>AddCommMonoid α<VAR>l : List α<GOAL>∑ i : Fin l.length, l[↑i] = l.sum
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>l : List α<GOAL>∏ i : Fin l.length, l[↑i] = l.prod
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid β<VAR>l : List α<VAR>f : α → β<GOAL>∏ i : Fin l.length, f l[↑i] = (List.map f l).prod
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid β<VAR>l : List α<VAR>f : α → β<GOAL>∑ i : Fin l.length, f l[↑i] = (List.map f l).sum
<VAR>β : Type u_2<VAR>CommMonoid β<VAR>n : ℕ<VAR>x : β<VAR>f : Fin n → β<GOAL>∏ i : Fin n.succ, Fin.cons x f i = x * ∏ i : Fin n, f i
<VAR>β : Type u_2<VAR>AddCommMonoid β<VAR>n : ℕ<VAR>x : β<VAR>f : Fin n → β<GOAL>∑ i : Fin n.succ, Fin.cons x f i = x + ∑ i : Fin n, f i
<VAR>β : Type u_2<VAR>AddCommMonoid β<VAR>f : Fin 1 → β<GOAL>∑ i : Fin 1, f i = f 0
<VAR>β : Type u_2<VAR>CommMonoid β<VAR>f : Fin 1 → β<GOAL>∏ i : Fin 1, f i = f 0
<VAR>β : Type u_2<VAR>CommMonoid β<VAR>f : Fin 2 → β<GOAL>∏ i : Fin 2, f i = f 0 * f 1
<VAR>β : Type u_2<VAR>AddCommMonoid β<VAR>f : Fin 2 → β<GOAL>∑ i : Fin 2, f i = f 0 + f 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid β<VAR>f : α → β<VAR>a b : α<GOAL>∏ i : Fin (Nat.succ 0).succ, f (![a, b] i) = f a * f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid β<VAR>f : α → β<VAR>a b : α<GOAL>∑ i : Fin (Nat.succ 0).succ, f (![a, b] i) = f a + f b
<VAR>β : Type u_2<VAR>CommMonoid β<VAR>f : Fin 3 → β<GOAL>∏ i : Fin 3, f i = f 0 * f 1 * f 2
<VAR>β : Type u_2<VAR>AddCommMonoid β<VAR>f : Fin 3 → β<GOAL>∑ i : Fin 3, f i = f 0 + f 1 + f 2
<VAR>β : Type u_2<VAR>AddCommMonoid β<VAR>f : Fin 4 → β<GOAL>∑ i : Fin 4, f i = f 0 + f 1 + f 2 + f 3
<VAR>β : Type u_2<VAR>CommMonoid β<VAR>f : Fin 4 → β<GOAL>∏ i : Fin 4, f i = f 0 * f 1 * f 2 * f 3
<VAR>β : Type u_2<VAR>CommMonoid β<VAR>f : Fin 5 → β<GOAL>∏ i : Fin 5, f i = f 0 * f 1 * f 2 * f 3 * f 4
<VAR>β : Type u_2<VAR>AddCommMonoid β<VAR>f : Fin 5 → β<GOAL>∑ i : Fin 5, f i = f 0 + f 1 + f 2 + f 3 + f 4
<VAR>β : Type u_2<VAR>CommMonoid β<VAR>f : Fin 6 → β<GOAL>∏ i : Fin 6, f i = f 0 * f 1 * f 2 * f 3 * f 4 * f 5
<VAR>β : Type u_2<VAR>AddCommMonoid β<VAR>f : Fin 6 → β<GOAL>∑ i : Fin 6, f i = f 0 + f 1 + f 2 + f 3 + f 4 + f 5