ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>Mul G<VAR>f g : MonoidAlgebra k G<VAR>x : G<VAR>s : Finset (G × G)<VAR>hs : ∀ {p : G × G}, p ∈ s ↔ p.1 * p.2 = x<GOAL>(f * g) x = ∑ p ∈ s, f p.1 * g p.2
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>Mul G<VAR>a₁ a₂ : G<VAR>b₁ b₂ : k<GOAL>MonoidAlgebra.single a₁ b₁ * MonoidAlgebra.single a₂ b₂ = MonoidAlgebra.single (a₁ * a₂) (b₁ * b₂)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>Mul G<VAR>a₁ a₂ : G<VAR>b₁ b₂ : k<VAR>ha : Commute a₁ a₂<VAR>hb : Commute b₁ b₂<GOAL>Commute (MonoidAlgebra.single a₁ b₁) (MonoidAlgebra.single a₂ b₂)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>Mul G<VAR>a : G<VAR>b : k<VAR>ha : ∀ (a' : G), Commute a a'<VAR>hb : ∀ (b' : k), Commute b b'<VAR>f : MonoidAlgebra k G<GOAL>Commute (MonoidAlgebra.single a b) f
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>Monoid G<VAR>a : G<VAR>b : k<VAR>n : ℕ<GOAL>MonoidAlgebra.single a b ^ n = MonoidAlgebra.single (a ^ n) (b ^ n)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>α₂ : Type u_5<VAR>Semiring β<VAR>One α<VAR>One α₂<VAR>F : Type u_6<VAR>FunLike F α α₂<VAR>OneHomClass F α α₂<VAR>f : F<GOAL>MonoidAlgebra.mapDomain (⇑f) 1 = 1
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>α₂ : Type u_5<VAR>Semiring β<VAR>Mul α<VAR>Mul α₂<VAR>F : Type u_6<VAR>FunLike F α α₂<VAR>MulHomClass F α α₂<VAR>f : F<VAR>x y : MonoidAlgebra β α<GOAL>MonoidAlgebra.mapDomain (⇑f) (x * y) = MonoidAlgebra.mapDomain (⇑f) x * MonoidAlgebra.mapDomain (⇑f) y
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>Mul G<VAR>a : G<GOAL>(MonoidAlgebra.ofMagma k G) a = MonoidAlgebra.single a 1
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>MulOneClass G<VAR>a : G<GOAL>(MonoidAlgebra.of k G) a = MonoidAlgebra.single a 1
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>MulOneClass G<VAR>g : G<VAR>r : k<GOAL>r • (MonoidAlgebra.of k G) g = MonoidAlgebra.single g r
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>MulOneClass G<VAR>Nontrivial k<GOAL>Function.Injective ⇑(MonoidAlgebra.of k G)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>MulOneClass G<VAR>a : G<VAR>h : ∀ (a' : G), Commute a a'<VAR>f : MonoidAlgebra k G<GOAL>Commute ((MonoidAlgebra.of k G) a) f
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>MulOneClass G<VAR>a : k × G<GOAL>MonoidAlgebra.singleHom a = MonoidAlgebra.single a.2 a.1
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>Mul G<VAR>f : MonoidAlgebra k G<VAR>r : k<VAR>x y z : G<VAR>H : ∀ (a : G), a * x = z ↔ a = y<GOAL>(f * MonoidAlgebra.single x r) z = f y * r
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>MulOneClass G<VAR>f : MonoidAlgebra k G<VAR>r : k<VAR>x : G<GOAL>(f * MonoidAlgebra.single 1 r) x = f x * r
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>Mul G<VAR>r : k<VAR>g g' : G<VAR>x : MonoidAlgebra k G<VAR>h : ¬∃ d, g' = d * g<GOAL>(x * MonoidAlgebra.single g r) g' = 0
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>Mul G<VAR>f : MonoidAlgebra k G<VAR>r : k<VAR>x y z : G<VAR>H : ∀ (a : G), x * a = y ↔ a = z<GOAL>(MonoidAlgebra.single x r * f) y = r * f z
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>MulOneClass G<VAR>f : MonoidAlgebra k G<VAR>r : k<VAR>x : G<GOAL>(MonoidAlgebra.single 1 r * f) x = r * f x
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>Mul G<VAR>r : k<VAR>g g' : G<VAR>x : MonoidAlgebra k G<VAR>h : ¬∃ d, g' = g * d<GOAL>(MonoidAlgebra.single g r * x) g' = 0
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>MulOneClass G<VAR>R : Type u_3<VAR>Semiring R<VAR>f : k →+* R<VAR>g : G →* R<VAR>c : k<VAR>φ : MonoidAlgebra k G<GOAL>(MonoidAlgebra.liftNC ↑f ⇑g) (c • φ) = f c * (MonoidAlgebra.liftNC ↑f ⇑g) φ
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>Mul G<VAR>A : Type u₃<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction k A<VAR>φ₁ φ₂ : MonoidAlgebra k G →ₙₐ[k] A<VAR>h : ∀ (x : G), φ₁ (MonoidAlgebra.single x 1) = φ₂ (MonoidAlgebra.single x 1)<GOAL>φ₁ = φ₂
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>Mul G<VAR>A : Type u₃<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction k A<VAR>φ₁ φ₂ : MonoidAlgebra k G →ₙₐ[k] A<VAR>h : φ₁.toMulHom.comp (MonoidAlgebra.ofMagma k G) = φ₂.toMulHom.comp (MonoidAlgebra.ofMagma k G)<GOAL>φ₁ = φ₂
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>Mul G<VAR>A : Type u₃<VAR>NonUnitalNonAssocSemiring A<VAR>Module k A<VAR>IsScalarTower k A A<VAR>SMulCommClass k A A<VAR>F : MonoidAlgebra k G →ₙₐ[k] A<GOAL>(MonoidAlgebra.liftMagma k).symm F = F.toMulHom.comp (MonoidAlgebra.ofMagma k G)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>Mul G<VAR>A : Type u₃<VAR>NonUnitalNonAssocSemiring A<VAR>Module k A<VAR>IsScalarTower k A A<VAR>SMulCommClass k A A<VAR>f : G →ₙ* A<VAR>a : MonoidAlgebra k G<GOAL>((MonoidAlgebra.liftMagma k) f) a = Finsupp.sum a fun m t => t • f m
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>CommSemiring k<VAR>MulOneClass G<VAR>r : k<VAR>f : MonoidAlgebra k G<GOAL>MonoidAlgebra.single 1 r * f = f * MonoidAlgebra.single 1 r
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>MulOneClass G<GOAL>∀ (a : k), MonoidAlgebra.singleOneRingHom a = (↑(Finsupp.singleAddHom 1)).toFun a
<VAR>G : Type u₂<VAR>k : Type u_3<VAR>H : Type u_4<VAR>F : Type u_5<VAR>Semiring k<VAR>Monoid G<VAR>Monoid H<VAR>FunLike F G H<VAR>MonoidHomClass F G H<VAR>f : F<GOAL>∀ (a : G →₀ k), (MonoidAlgebra.mapDomainRingHom k f) a = (↑(Finsupp.mapDomain.addMonoidHom ⇑f)).toFun a
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>R : Type u_3<VAR>Semiring k<VAR>MulOneClass G<VAR>Semiring R<VAR>f g : MonoidAlgebra k G →+* R<VAR>h₁ : ∀ (b : k), f (MonoidAlgebra.single 1 b) = g (MonoidAlgebra.single 1 b)<VAR>h_of : ∀ (a : G), f (MonoidAlgebra.single a 1) = g (MonoidAlgebra.single a 1)<GOAL>f = g
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>R : Type u_3<VAR>Semiring k<VAR>MulOneClass G<VAR>Semiring R<VAR>f g : MonoidAlgebra k G →+* R<VAR>h₁ : f.comp MonoidAlgebra.singleOneRingHom = g.comp MonoidAlgebra.singleOneRingHom<VAR>h_of : (↑f).comp (MonoidAlgebra.of k G) = (↑g).comp (MonoidAlgebra.of k G)<GOAL>f = g
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>A : Type u_3<VAR>CommSemiring k<VAR>Semiring A<VAR>Algebra k A<VAR>Monoid G<GOAL>∀ (a : A), MonoidAlgebra.singleOneAlgHom a = Finsupp.single 1 a
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>A : Type u_3<VAR>CommSemiring k<VAR>Semiring A<VAR>Algebra k A<VAR>Monoid G<GOAL>⇑(algebraMap k (MonoidAlgebra A G)) = MonoidAlgebra.single 1 ∘ ⇑(algebraMap k A)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>CommSemiring k<VAR>Monoid G<VAR>a : G<VAR>b : k<GOAL>MonoidAlgebra.single a b = (algebraMap k (MonoidAlgebra k G)) b * (MonoidAlgebra.of k G) a
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>A : Type u_3<VAR>CommSemiring k<VAR>Semiring A<VAR>Algebra k A<VAR>Monoid G<VAR>a : G<VAR>b : k<GOAL>MonoidAlgebra.single a ((algebraMap k A) b) = (algebraMap k (MonoidAlgebra A G)) b * (MonoidAlgebra.of A G) a
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>Monoid G<VAR>p : MonoidAlgebra k G → Prop<VAR>f : MonoidAlgebra k G<VAR>hM : ∀ (g : G), p ((MonoidAlgebra.of k G) g)<VAR>hadd : ∀ (f g : MonoidAlgebra k G), p f → p g → p (f + g)<VAR>hsmul : ∀ (r : k) (f : MonoidAlgebra k G), p f → p (r • f)<GOAL>p f
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>CommSemiring k<VAR>Monoid G<VAR>A : Type u₃<VAR>Semiring A<VAR>Algebra k A<VAR>φ₁ φ₂ : MonoidAlgebra k G →ₐ[k] A<VAR>h : ∀ (x : G), φ₁ (MonoidAlgebra.single x 1) = φ₂ (MonoidAlgebra.single x 1)<GOAL>φ₁ = φ₂
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>CommSemiring k<VAR>Monoid G<VAR>A : Type u₃<VAR>Semiring A<VAR>Algebra k A<VAR>φ₁ φ₂ : MonoidAlgebra k G →ₐ[k] A<VAR>h : (↑φ₁).comp (MonoidAlgebra.of k G) = (↑φ₂).comp (MonoidAlgebra.of k G)<GOAL>φ₁ = φ₂
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>CommSemiring k<VAR>Monoid G<VAR>A : Type u₃<VAR>Semiring A<VAR>Algebra k A<VAR>F : G →* A<VAR>f : MonoidAlgebra k G<GOAL>((MonoidAlgebra.lift k G A) F) f = Finsupp.sum f fun a b => (algebraMap k A) b * F a
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>CommSemiring k<VAR>Monoid G<VAR>A : Type u₃<VAR>Semiring A<VAR>Algebra k A<VAR>F : G →* A<VAR>f : MonoidAlgebra k G<GOAL>((MonoidAlgebra.lift k G A) F) f = Finsupp.sum f fun a b => b • F a
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>CommSemiring k<VAR>Monoid G<VAR>A : Type u₃<VAR>Semiring A<VAR>Algebra k A<VAR>F : G →* A<GOAL>⇑((MonoidAlgebra.lift k G A) F) = ⇑(MonoidAlgebra.liftNC ↑(algebraMap k A) ⇑F)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>CommSemiring k<VAR>Monoid G<VAR>A : Type u₃<VAR>Semiring A<VAR>Algebra k A<VAR>F : MonoidAlgebra k G →ₐ[k] A<VAR>x : G<GOAL>((MonoidAlgebra.lift k G A).symm F) x = F (MonoidAlgebra.single x 1)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>CommSemiring k<VAR>Monoid G<VAR>A : Type u₃<VAR>Semiring A<VAR>Algebra k A<VAR>F : G →* A<VAR>a : G<VAR>b : k<GOAL>((MonoidAlgebra.lift k G A) F) (MonoidAlgebra.single a b) = b • F a
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>CommSemiring k<VAR>Monoid G<VAR>A : Type u₃<VAR>Semiring A<VAR>Algebra k A<VAR>F : G →* A<VAR>x : G<GOAL>((MonoidAlgebra.lift k G A) F) ((MonoidAlgebra.of k G) x) = F x
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>CommSemiring k<VAR>Monoid G<VAR>A : Type u₃<VAR>Semiring A<VAR>Algebra k A<VAR>F : MonoidAlgebra k G →ₐ[k] A<GOAL>F = (MonoidAlgebra.lift k G A) ((↑F).comp (MonoidAlgebra.of k G))
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>CommSemiring k<VAR>Monoid G<VAR>A : Type u₃<VAR>Semiring A<VAR>Algebra k A<VAR>F : MonoidAlgebra k G →ₐ[k] A<VAR>f : MonoidAlgebra k G<GOAL>F f = Finsupp.sum f fun a b => b • F (MonoidAlgebra.single a 1)
<VAR>k : Type u_4<VAR>A : Type u_5<VAR>CommSemiring k<VAR>Semiring A<VAR>Algebra k A<VAR>G : Type u_6<VAR>H : Type u_7<VAR>F : Type u_8<VAR>Mul G<VAR>Mul H<VAR>FunLike F G H<VAR>MulHomClass F G H<VAR>f : F<GOAL>∀ (a : G →₀ A), (MonoidAlgebra.mapDomainNonUnitalAlgHom k A f) a = (↑(Finsupp.mapDomain.addMonoidHom ⇑f)).toFun a
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>CommSemiring k<VAR>Monoid G<VAR>Monoid H<VAR>A : Type u₃<VAR>Semiring A<VAR>Algebra k A<VAR>F : Type u_4<VAR>FunLike F G H<VAR>MonoidHomClass F G H<VAR>f : F<VAR>r : k<GOAL>MonoidAlgebra.mapDomain (⇑f) ((algebraMap k (MonoidAlgebra A G)) r) = (algebraMap k (MonoidAlgebra A H)) r
<VAR>G : Type u₂<VAR>Monoid G<VAR>k : Type u_4<VAR>A : Type u_5<VAR>CommSemiring k<VAR>Semiring A<VAR>Algebra k A<VAR>H : Type u_6<VAR>F : Type u_7<VAR>Monoid H<VAR>FunLike F G H<VAR>MonoidHomClass F G H<VAR>f : F<GOAL>∀ (a : G →₀ A), (MonoidAlgebra.mapDomainAlgHom k A f) a = Finsupp.mapDomain (⇑f) a
<VAR>G : Type u₂<VAR>Monoid G<VAR>k : Type u_4<VAR>A : Type u_5<VAR>CommSemiring k<VAR>Semiring A<VAR>Algebra k A<GOAL>MonoidAlgebra.mapDomainAlgHom k A (MonoidHom.id G) = AlgHom.id k (MonoidAlgebra A G)
<VAR>k : Type u_4<VAR>A : Type u_5<VAR>G₁ : Type u_6<VAR>G₂ : Type u_7<VAR>G₃ : Type u_8<VAR>CommSemiring k<VAR>Semiring A<VAR>Algebra k A<VAR>Monoid G₁<VAR>Monoid G₂<VAR>Monoid G₃<VAR>f : G₁ →* G₂<VAR>g : G₂ →* G₃<GOAL>MonoidAlgebra.mapDomainAlgHom k A (g.comp f) = (MonoidAlgebra.mapDomainAlgHom k A g).comp (MonoidAlgebra.mapDomainAlgHom k A f)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>CommSemiring k<VAR>Monoid G<VAR>Monoid H<VAR>A : Type u₃<VAR>Semiring A<VAR>Algebra k A<VAR>e : G ≃* H<GOAL>↑(MonoidAlgebra.domCongr k A e) = MonoidAlgebra.mapDomainAlgHom k A e
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>CommSemiring k<VAR>Monoid G<VAR>Monoid H<VAR>A : Type u₃<VAR>Semiring A<VAR>Algebra k A<VAR>e : G ≃* H<VAR>f : MonoidAlgebra A G<VAR>h : H<GOAL>((MonoidAlgebra.domCongr k A e) f) h = f (e.symm h)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>CommSemiring k<VAR>Monoid G<VAR>Monoid H<VAR>A : Type u₃<VAR>Semiring A<VAR>Algebra k A<VAR>e : G ≃* H<VAR>f : MonoidAlgebra A G<GOAL>((MonoidAlgebra.domCongr k A e) f).support = Finset.map (↑e).toEmbedding f.support
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>CommSemiring k<VAR>Monoid G<VAR>Monoid H<VAR>A : Type u₃<VAR>Semiring A<VAR>Algebra k A<VAR>e : G ≃* H<VAR>g : G<VAR>a : A<GOAL>(MonoidAlgebra.domCongr k A e) (MonoidAlgebra.single g a) = MonoidAlgebra.single (e g) a
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>CommSemiring k<VAR>Monoid G<VAR>A : Type u₃<VAR>Semiring A<VAR>Algebra k A<GOAL>MonoidAlgebra.domCongr k A (MulEquiv.refl G) = AlgEquiv.refl
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>CommSemiring k<VAR>Monoid G<VAR>Monoid H<VAR>A : Type u₃<VAR>Semiring A<VAR>Algebra k A<VAR>e : G ≃* H<GOAL>(MonoidAlgebra.domCongr k A e).symm = MonoidAlgebra.domCongr k A e.symm
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Monoid G<VAR>CommSemiring k<VAR>V : Type u₃<VAR>AddCommMonoid V<VAR>Module k V<VAR>Module (MonoidAlgebra k G) V<VAR>IsScalarTower k (MonoidAlgebra k G) V<VAR>g : G<VAR>v : V<GOAL>(MonoidAlgebra.GroupSMul.linearMap k V g) v = MonoidAlgebra.single g 1 • v
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Monoid G<VAR>CommSemiring k<VAR>V : Type u₃<VAR>W : Type u₄<VAR>AddCommMonoid V<VAR>Module k V<VAR>Module (MonoidAlgebra k G) V<VAR>IsScalarTower k (MonoidAlgebra k G) V<VAR>AddCommMonoid W<VAR>Module k W<VAR>Module (MonoidAlgebra k G) W<VAR>IsScalarTower k (MonoidAlgebra k G) W<VAR>f : V →ₗ[k] W<VAR>h : ∀ (g : G) (v : V), f (MonoidAlgebra.single g 1 • v) = MonoidAlgebra.single g 1 • f v<VAR>v : V<GOAL>(MonoidAlgebra.equivariantOfLinearOfComm f h) v = f v
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>ι : Type ui<VAR>CommSemiring k<VAR>CommMonoid G<VAR>s : Finset ι<VAR>a : ι → G<VAR>b : ι → k<GOAL>∏ i ∈ s, MonoidAlgebra.single (a i) (b i) = MonoidAlgebra.single (∏ i ∈ s, a i) (∏ i ∈ s, b i)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>Group G<VAR>f : MonoidAlgebra k G<VAR>r : k<VAR>x y : G<GOAL>(f * MonoidAlgebra.single x r) y = f (y * x⁻¹) * r
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>Group G<VAR>r : k<VAR>x : G<VAR>f : MonoidAlgebra k G<VAR>y : G<GOAL>(MonoidAlgebra.single x r * f) y = r * f (x⁻¹ * y)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>Group G<VAR>f g : MonoidAlgebra k G<VAR>x : G<GOAL>(f * g) x = Finsupp.sum f fun a b => b * g (a⁻¹ * x)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>Group G<VAR>f g : MonoidAlgebra k G<VAR>x : G<GOAL>(f * g) x = Finsupp.sum g fun a b => f (x * a⁻¹) * b
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>Monoid G<GOAL>∀ (a : (G →₀ k)ᵐᵒᵖ), MonoidAlgebra.opRingEquiv a = Finsupp.equivMapDomain MulOpposite.opEquiv (Finsupp.mapRange MulOpposite.op ⋯ (MulOpposite.unop a))
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>Monoid G<GOAL>∀ (a : Gᵐᵒᵖ →₀ kᵐᵒᵖ), MonoidAlgebra.opRingEquiv.symm a = MulOpposite.op (Finsupp.mapRange MulOpposite.unop ⋯ (Finsupp.equivMapDomain MulOpposite.opEquiv.symm a))
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>Monoid G<VAR>r : k<VAR>x : G<GOAL>MonoidAlgebra.opRingEquiv (MulOpposite.op (MonoidAlgebra.single x r)) = MonoidAlgebra.single (MulOpposite.op x) (MulOpposite.op r)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>Monoid G<VAR>r : kᵐᵒᵖ<VAR>x : Gᵐᵒᵖ<GOAL>MonoidAlgebra.opRingEquiv.symm (MonoidAlgebra.single x r) = MulOpposite.op (MonoidAlgebra.single (MulOpposite.unop x) (MulOpposite.unop r))
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>a : G<GOAL>AddMonoidAlgebra.single a 0 = 0
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>a : G<VAR>b₁ b₂ : k<GOAL>AddMonoidAlgebra.single a (b₁ + b₂) = AddMonoidAlgebra.single a b₁ + AddMonoidAlgebra.single a b₂
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>N : Type u_3<VAR>AddCommMonoid N<VAR>a : G<VAR>b : k<VAR>h : G → k → N<VAR>h_zero : h a 0 = 0<GOAL>Finsupp.sum (AddMonoidAlgebra.single a b) h = h a b
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>f : AddMonoidAlgebra k G<GOAL>Finsupp.sum f AddMonoidAlgebra.single = f
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>a a' : G<VAR>b : k<VAR>Decidable (a = a')<GOAL>(AddMonoidAlgebra.single a b) a' = if a = a' then b else 0
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>a : G<VAR>b : k<GOAL>AddMonoidAlgebra.single a b = 0 ↔ b = 0
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>k' : Type u_3<VAR>G' : Type u_4<VAR>Semiring k'<VAR>f : G → G'<VAR>s : AddMonoidAlgebra k' G<VAR>v : G → k' → AddMonoidAlgebra k G<GOAL>AddMonoidAlgebra.mapDomain f (Finsupp.sum s v) = Finsupp.sum s fun a b => AddMonoidAlgebra.mapDomain f (v a b)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>G' : Type u_3<VAR>f : G → G'<VAR>a : G<VAR>b : k<GOAL>AddMonoidAlgebra.mapDomain f (AddMonoidAlgebra.single a b) = AddMonoidAlgebra.single (f a) b
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>R : Type u_2<VAR>Semiring k<VAR>NonUnitalNonAssocSemiring R<VAR>f : k →+ R<VAR>g : Multiplicative G → R<VAR>a : G<VAR>b : k<GOAL>(AddMonoidAlgebra.liftNC f g) (AddMonoidAlgebra.single a b) = f b * g (Multiplicative.ofAdd a)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>Add G<VAR>f g : AddMonoidAlgebra k G<GOAL>f * g = Finsupp.sum f fun a₁ b₁ => Finsupp.sum g fun a₂ b₂ => AddMonoidAlgebra.single (a₁ + a₂) (b₁ * b₂)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>R : Type u_2<VAR>Semiring k<VAR>Add G<VAR>Semiring R<VAR>g_hom : Type u_3<VAR>FunLike g_hom (Multiplicative G) R<VAR>MulHomClass g_hom (Multiplicative G) R<VAR>f : k →+* R<VAR>g : g_hom<VAR>a b : AddMonoidAlgebra k G<VAR>h_comm : ∀ {x y : G}, y ∈ a.support → Commute (f (b x)) (g (Multiplicative.ofAdd y))<GOAL>(AddMonoidAlgebra.liftNC ↑f ⇑g) (a * b) = (AddMonoidAlgebra.liftNC ↑f ⇑g) a * (AddMonoidAlgebra.liftNC ↑f ⇑g) b
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>Zero G<GOAL>1 = AddMonoidAlgebra.single 0 1
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>R : Type u_2<VAR>Semiring k<VAR>Zero G<VAR>NonAssocSemiring R<VAR>g_hom : Type u_3<VAR>FunLike g_hom (Multiplicative G) R<VAR>OneHomClass g_hom (Multiplicative G) R<VAR>f : k →+* R<VAR>g : g_hom<GOAL>(AddMonoidAlgebra.liftNC ↑f ⇑g) 1 = 1
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>AddZeroClass G<VAR>n : ℕ<GOAL>↑n = AddMonoidAlgebra.single 0 ↑n
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Ring k<VAR>AddZeroClass G<VAR>z : ℤ<GOAL>↑z = AddMonoidAlgebra.single 0 ↑z
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>DecidableEq G<VAR>Add G<VAR>f g : AddMonoidAlgebra k G<VAR>x : G<GOAL>(f * g) x = Finsupp.sum f fun a₁ b₁ => Finsupp.sum g fun a₂ b₂ => if a₁ + a₂ = x then b₁ * b₂ else 0
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>Add G<VAR>f g : AddMonoidAlgebra k G<VAR>x : G<VAR>s : Finset (G × G)<VAR>hs : ∀ {p : G × G}, p ∈ s ↔ p.1 + p.2 = x<GOAL>(f * g) x = ∑ p ∈ s, f p.1 * g p.2
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>Add G<VAR>a₁ a₂ : G<VAR>b₁ b₂ : k<GOAL>AddMonoidAlgebra.single a₁ b₁ * AddMonoidAlgebra.single a₂ b₂ = AddMonoidAlgebra.single (a₁ + a₂) (b₁ * b₂)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>Add G<VAR>a₁ a₂ : G<VAR>b₁ b₂ : k<VAR>ha : AddCommute a₁ a₂<VAR>hb : Commute b₁ b₂<GOAL>Commute (AddMonoidAlgebra.single a₁ b₁) (AddMonoidAlgebra.single a₂ b₂)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>AddMonoid G<VAR>a : G<VAR>b : k<VAR>n : ℕ<GOAL>AddMonoidAlgebra.single a b ^ n = AddMonoidAlgebra.single (n • a) (b ^ n)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>α₂ : Type u_5<VAR>Semiring β<VAR>Zero α<VAR>Zero α₂<VAR>F : Type u_6<VAR>FunLike F α α₂<VAR>ZeroHomClass F α α₂<VAR>f : F<GOAL>AddMonoidAlgebra.mapDomain (⇑f) 1 = 1
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>α₂ : Type u_5<VAR>Semiring β<VAR>Add α<VAR>Add α₂<VAR>F : Type u_6<VAR>FunLike F α α₂<VAR>AddHomClass F α α₂<VAR>f : F<VAR>x y : AddMonoidAlgebra β α<GOAL>AddMonoidAlgebra.mapDomain (⇑f) (x * y) = AddMonoidAlgebra.mapDomain (⇑f) x * AddMonoidAlgebra.mapDomain (⇑f) y
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>Add G<VAR>a : Multiplicative G<GOAL>(AddMonoidAlgebra.ofMagma k G) a = AddMonoidAlgebra.single a 1
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>AddZeroClass G<VAR>a : Multiplicative G<GOAL>(AddMonoidAlgebra.of k G) a = AddMonoidAlgebra.single (Multiplicative.toAdd a) 1
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>a : G<GOAL>AddMonoidAlgebra.of' k G a = AddMonoidAlgebra.single a 1
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>AddZeroClass G<VAR>a : G<GOAL>AddMonoidAlgebra.of' k G a = (AddMonoidAlgebra.of k G) (Multiplicative.ofAdd a)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>Nontrivial k<VAR>AddZeroClass G<GOAL>Function.Injective ⇑(AddMonoidAlgebra.of k G)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>AddZeroClass G<VAR>a : G<VAR>h : ∀ (a' : G), AddCommute a a'<VAR>f : AddMonoidAlgebra k G<GOAL>Commute (AddMonoidAlgebra.of' k G a) f
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>AddZeroClass G<VAR>a : k × Multiplicative G<GOAL>AddMonoidAlgebra.singleHom a = AddMonoidAlgebra.single (Multiplicative.toAdd a.2) a.1
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>Add G<VAR>f : AddMonoidAlgebra k G<VAR>r : k<VAR>x y z : G<VAR>H : ∀ (a : G), a + x = z ↔ a = y<GOAL>(f * AddMonoidAlgebra.single x r) z = f y * r
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>AddZeroClass G<VAR>f : AddMonoidAlgebra k G<VAR>r : k<VAR>x : G<GOAL>(f * AddMonoidAlgebra.single 0 r) x = f x * r
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>Add G<VAR>r : k<VAR>g g' : G<VAR>x : AddMonoidAlgebra k G<VAR>h : ¬∃ d, g' = d + g<GOAL>(x * AddMonoidAlgebra.single g r) g' = 0
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>Add G<VAR>f : AddMonoidAlgebra k G<VAR>r : k<VAR>x y z : G<VAR>H : ∀ (a : G), x + a = y ↔ a = z<GOAL>(AddMonoidAlgebra.single x r * f) y = r * f z
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>AddZeroClass G<VAR>f : AddMonoidAlgebra k G<VAR>r : k<VAR>x : G<GOAL>(AddMonoidAlgebra.single 0 r * f) x = r * f x
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>Add G<VAR>r : k<VAR>g g' : G<VAR>x : AddMonoidAlgebra k G<VAR>h : ¬∃ d, g' = g + d<GOAL>(AddMonoidAlgebra.single g r * x) g' = 0
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>AddGroup G<VAR>f : AddMonoidAlgebra k G<VAR>r : k<VAR>x y : G<GOAL>(f * AddMonoidAlgebra.single x r) y = f (y - x) * r
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>AddGroup G<VAR>r : k<VAR>x : G<VAR>f : AddMonoidAlgebra k G<VAR>y : G<GOAL>(AddMonoidAlgebra.single x r * f) y = r * f (-x + y)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>R : Type u_3<VAR>AddZeroClass G<VAR>Semiring R<VAR>f : k →+* R<VAR>g : Multiplicative G →* R<VAR>c : k<VAR>φ : MonoidAlgebra k G<GOAL>(AddMonoidAlgebra.liftNC ↑f ⇑g) (c • φ) = f c * (AddMonoidAlgebra.liftNC ↑f ⇑g) φ
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>AddMonoid G<VAR>p : AddMonoidAlgebra k G → Prop<VAR>f : AddMonoidAlgebra k G<VAR>hM : ∀ (g : G), p ((AddMonoidAlgebra.of k G) (Multiplicative.ofAdd g))<VAR>hadd : ∀ (f g : AddMonoidAlgebra k G), p f → p g → p (f + g)<VAR>hsmul : ∀ (r : k) (f : AddMonoidAlgebra k G), p f → p (r • f)<GOAL>p f
<VAR>G : Type u₂<VAR>k : Type u_3<VAR>Semiring k<VAR>H : Type u_4<VAR>F : Type u_5<VAR>AddMonoid G<VAR>AddMonoid H<VAR>FunLike F G H<VAR>AddMonoidHomClass F G H<VAR>f : F<GOAL>∀ (a : G →₀ k), (AddMonoidAlgebra.mapDomainRingHom k f) a = (↑(Finsupp.mapDomain.addMonoidHom ⇑f)).toFun a
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>Add G<VAR>A : Type u₃<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction k A<VAR>φ₁ φ₂ : AddMonoidAlgebra k G →ₙₐ[k] A<VAR>h : ∀ (x : G), φ₁ (AddMonoidAlgebra.single x 1) = φ₂ (AddMonoidAlgebra.single x 1)<GOAL>φ₁ = φ₂
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>Add G<VAR>A : Type u₃<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction k A<VAR>φ₁ φ₂ : AddMonoidAlgebra k G →ₙₐ[k] A<VAR>h : φ₁.toMulHom.comp (AddMonoidAlgebra.ofMagma k G) = φ₂.toMulHom.comp (AddMonoidAlgebra.ofMagma k G)<GOAL>φ₁ = φ₂
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>Add G<VAR>A : Type u₃<VAR>NonUnitalNonAssocSemiring A<VAR>Module k A<VAR>IsScalarTower k A A<VAR>SMulCommClass k A A<VAR>f : Multiplicative G →ₙ* A<VAR>a : AddMonoidAlgebra k G<GOAL>((AddMonoidAlgebra.liftMagma k) f) a = Finsupp.sum a fun m t => t • f (Multiplicative.ofAdd m)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>Add G<VAR>A : Type u₃<VAR>NonUnitalNonAssocSemiring A<VAR>Module k A<VAR>IsScalarTower k A A<VAR>SMulCommClass k A A<VAR>F : AddMonoidAlgebra k G →ₙₐ[k] A<GOAL>(AddMonoidAlgebra.liftMagma k).symm F = F.toMulHom.comp (AddMonoidAlgebra.ofMagma k G)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>AddMonoid G<GOAL>∀ (a : k), AddMonoidAlgebra.singleZeroRingHom a = (↑(Finsupp.singleAddHom 0)).toFun a
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>R : Type u_3<VAR>Semiring k<VAR>AddMonoid G<VAR>Semiring R<VAR>f g : AddMonoidAlgebra k G →+* R<VAR>h₀ : ∀ (b : k), f (AddMonoidAlgebra.single 0 b) = g (AddMonoidAlgebra.single 0 b)<VAR>h_of : ∀ (a : G), f (AddMonoidAlgebra.single a 1) = g (AddMonoidAlgebra.single a 1)<GOAL>f = g