Documentation

Mathlib.Algebra.SkewMonoidAlgebra.Basic

Skew Monoid Algebras #

Given a monoid G and a ring k, the skew monoid algebra of G over k is the set of finitely supported functions f : G → k for which addition is defined pointwise and multiplication of two elements f and g is given by the finitely supported function whose value at a is the sum of f x * (x • g y) over all pairs x, y such that x * y = a, where • denotes the action of G on k. When this action is trivial, this product is the usual convolution product.

In fact the construction of the skew monoid algebra makes sense when G is not even a monoid, but merely a magma, i.e., when G carries a multiplication which is not required to satisfy any conditions at all, and k is a not-necessarily-associative semiring. In this case the construction yields a not-necessarily-unital, not-necessarily-associative algebra.

Main Definitions #

SkewMonoidAlgebra k G: the skew monoid algebra of G over k is the type of finite formal k-linear combinations of terms of G, endowed with a skewed convolution product.

TODO #

Define the skew convolution product.
Provide algebraic instances.

structure SkewMonoidAlgebra (k : Type u_1) (G : Type u_2) [Zero k] :

Type (max u_1 u_2)

The skew monoid algebra of G over k is the type of finite formal k-linear combinations of terms of G, endowed with a skewed convolution product.

ofFinsupp :: (

toFinsupp : G →₀ k
The natural map from SkewMonoidAlgebra k G to G →₀ k.

)

Instances For

@[simp]

theorem SkewMonoidAlgebra.eta {k : Type u_1} {G : Type u_2} [AddCommMonoid k] (f : SkewMonoidAlgebra k G) :

{ toFinsupp := f.toFinsupp } = f

instance SkewMonoidAlgebra.instZero {k : Type u_1} {G : Type u_2} [AddCommMonoid k] :

Zero (SkewMonoidAlgebra k G)

Equations

SkewMonoidAlgebra.instZero = { zero := { toFinsupp := 0 } }

instance SkewMonoidAlgebra.instAdd {k : Type u_1} {G : Type u_2} [AddCommMonoid k] :

Add (SkewMonoidAlgebra k G)

Equations

SkewMonoidAlgebra.instAdd = { add := SkewMonoidAlgebra.add✝ }

instance SkewMonoidAlgebra.instSMulZeroClass {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {S : Type u_3} [SMulZeroClass S k] :

SMulZeroClass S (SkewMonoidAlgebra k G)

Equations

SkewMonoidAlgebra.instSMulZeroClass = { smul := fun (s : S) (f : SkewMonoidAlgebra k G) => SkewMonoidAlgebra.smul✝ s f, smul_zero := ⋯ }

@[simp]

theorem SkewMonoidAlgebra.ofFinsupp_zero {k : Type u_1} {G : Type u_2} [AddCommMonoid k] :

{ toFinsupp := 0 } = 0

@[simp]

theorem SkewMonoidAlgebra.ofFinsupp_add {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {a b : G →₀ k} :

{ toFinsupp := a + b } = { toFinsupp := a } + { toFinsupp := b }

@[simp]

theorem SkewMonoidAlgebra.ofFinsupp_smul {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {S : Type u_3} [SMulZeroClass S k] (a : S) (b : G →₀ k) :

{ toFinsupp := a • b } = a • { toFinsupp := b }

@[simp]

theorem SkewMonoidAlgebra.toFinsupp_zero {k : Type u_1} {G : Type u_2} [AddCommMonoid k] :

toFinsupp 0 = 0

@[simp]

theorem SkewMonoidAlgebra.toFinsupp_add {k : Type u_1} {G : Type u_2} [AddCommMonoid k] (a b : SkewMonoidAlgebra k G) :

(a + b).toFinsupp = a.toFinsupp + b.toFinsupp

@[simp]

theorem SkewMonoidAlgebra.toFinsupp_smul {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {S : Type u_3} [SMulZeroClass S k] (a : S) (b : SkewMonoidAlgebra k G) :

(a • b).toFinsupp = a • b.toFinsupp

theorem IsSMulRegular.skewMonoidAlgebra {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {S : Type u_3} [Monoid S] [DistribMulAction S k] {a : S} (ha : IsSMulRegular k a) :

IsSMulRegular (SkewMonoidAlgebra k G) a

theorem SkewMonoidAlgebra.toFinsupp_injective {k : Type u_1} {G : Type u_2} [AddCommMonoid k] :

Function.Injective toFinsupp

@[simp]

theorem SkewMonoidAlgebra.toFinsupp_inj {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {a b : SkewMonoidAlgebra k G} :

a.toFinsupp = b.toFinsupp ↔ a = b

theorem SkewMonoidAlgebra.ofFinsupp_injective {k : Type u_1} {G : Type u_2} [AddCommMonoid k] :

Function.Injective ofFinsupp

theorem SkewMonoidAlgebra.ofFinsupp_inj {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {a b : G →₀ k} :

{ toFinsupp := a } = { toFinsupp := b } ↔ a = b

A more convenient spelling of SkewMonoidAlgebra.ofFinsupp.injEq in terms of Iff.

@[simp]

theorem SkewMonoidAlgebra.toFinsupp_eq_zero {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {a : SkewMonoidAlgebra k G} :

a.toFinsupp = 0 ↔ a = 0

@[simp]

theorem SkewMonoidAlgebra.ofFinsupp_eq_zero {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {a : G →₀ k} :

{ toFinsupp := a } = 0 ↔ a = 0

instance SkewMonoidAlgebra.instInhabited {k : Type u_1} {G : Type u_2} [AddCommMonoid k] :

Inhabited (SkewMonoidAlgebra k G)

Equations

SkewMonoidAlgebra.instInhabited = { default := 0 }

instance SkewMonoidAlgebra.instNontrivial {k : Type u_1} {G : Type u_2} [AddCommMonoid k] [Nontrivial k] [Nonempty G] :

Nontrivial (SkewMonoidAlgebra k G)

instance SkewMonoidAlgebra.instAddCommMonoid {k : Type u_1} {G : Type u_2} [AddCommMonoid k] :

AddCommMonoid (SkewMonoidAlgebra k G)

Equations

One or more equations did not get rendered due to their size.

def SkewMonoidAlgebra.support {k : Type u_1} {G : Type u_2} [AddCommMonoid k] :

SkewMonoidAlgebra k G → Finset G

For f : SkewMonoidAlgebra k G, f.support is the set of all a ∈ G such that f a ≠ 0.

Equations

{ toFinsupp := p }.support = p.support

Instances For

@[simp]

theorem SkewMonoidAlgebra.support_ofFinsupp {k : Type u_1} {G : Type u_2} [AddCommMonoid k] (p : G →₀ k) :

{ toFinsupp := p }.support = p.support

theorem SkewMonoidAlgebra.support_toFinsupp {k : Type u_1} {G : Type u_2} [AddCommMonoid k] (p : SkewMonoidAlgebra k G) :

p.toFinsupp.support = p.support

@[simp]

theorem SkewMonoidAlgebra.support_zero {k : Type u_1} {G : Type u_2} [AddCommMonoid k] :

support 0 = ∅

@[simp]

theorem SkewMonoidAlgebra.support_eq_empty {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {p : SkewMonoidAlgebra k G} :

p.support = ∅ ↔ p = 0

def SkewMonoidAlgebra.coeff {k : Type u_1} {G : Type u_2} [AddCommMonoid k] :

SkewMonoidAlgebra k G → G → k

coeff f a (often denoted f.coeff a) is the coefficient of a in f.

Equations

{ toFinsupp := p }.coeff = ⇑p

Instances For

@[simp]

theorem SkewMonoidAlgebra.coeff_ofFinsupp {k : Type u_1} {G : Type u_2} [AddCommMonoid k] (p : G →₀ k) :

{ toFinsupp := p }.coeff = ⇑p

theorem SkewMonoidAlgebra.coeff_injective {k : Type u_1} {G : Type u_2} [AddCommMonoid k] :

Function.Injective coeff

@[simp]

theorem SkewMonoidAlgebra.coeff_inj {k : Type u_1} {G : Type u_2} [AddCommMonoid k] (p q : SkewMonoidAlgebra k G) :

p.coeff = q.coeff ↔ p = q

@[simp]

theorem SkewMonoidAlgebra.toFinsupp_apply {k : Type u_1} {G : Type u_2} [AddCommMonoid k] (f : SkewMonoidAlgebra k G) (g : G) :

f.toFinsupp g = f.coeff g

@[simp]

theorem SkewMonoidAlgebra.coeff_zero {k : Type u_1} {G : Type u_2} [AddCommMonoid k] (g : G) :

coeff 0 g = 0

@[simp]

theorem SkewMonoidAlgebra.mem_support_iff {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {f : SkewMonoidAlgebra k G} {a : G} :

a ∈ f.support ↔ f.coeff a ≠ 0

theorem SkewMonoidAlgebra.notMem_support_iff {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {f : SkewMonoidAlgebra k G} {a : G} :

a ∉ f.support ↔ f.coeff a = 0

@[deprecated SkewMonoidAlgebra.notMem_support_iff (since := "2025-05-23")]

theorem SkewMonoidAlgebra.not_mem_support_iff {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {f : SkewMonoidAlgebra k G} {a : G} :

a ∉ f.support ↔ f.coeff a = 0

Alias of SkewMonoidAlgebra.notMem_support_iff.

theorem SkewMonoidAlgebra.ext_iff {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {p q : SkewMonoidAlgebra k G} :

p = q ↔ ∀ (n : G), p.coeff n = q.coeff n

theorem SkewMonoidAlgebra.ext {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {p q : SkewMonoidAlgebra k G} :

(∀ (a : G), p.coeff a = q.coeff a) → p = q

@[simp]

theorem SkewMonoidAlgebra.coeff_add {k : Type u_1} {G : Type u_2} [AddCommMonoid k] (p q : SkewMonoidAlgebra k G) (a : G) :

(p + q).coeff a = p.coeff a + q.coeff a

@[simp]

theorem SkewMonoidAlgebra.coeff_smul {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {S : Type u_3} [SMulZeroClass S k] (r : S) (p : SkewMonoidAlgebra k G) (a : G) :

(r • p).coeff a = r • p.coeff a

def SkewMonoidAlgebra.single {k : Type u_1} {G : Type u_2} [AddCommMonoid k] (a : G) (b : k) :

SkewMonoidAlgebra k G

single a b is the finitely supported function with value b at a and zero otherwise.

Equations

SkewMonoidAlgebra.single a b = { toFinsupp := Finsupp.single a b }

Instances For

@[simp]

theorem SkewMonoidAlgebra.toFinsupp_single {k : Type u_1} {G : Type u_2} [AddCommMonoid k] (a : G) (b : k) :

(single a b).toFinsupp = Finsupp.single a b

@[simp]

theorem SkewMonoidAlgebra.ofFinsupp_single {k : Type u_1} {G : Type u_2} [AddCommMonoid k] (a : G) (b : k) :

{ toFinsupp := Finsupp.single a b } = single a b

theorem SkewMonoidAlgebra.coeff_single {k : Type u_1} {G : Type u_2} [AddCommMonoid k] (a : G) (b : k) [DecidableEq G] :

(single a b).coeff = Pi.single a b

theorem SkewMonoidAlgebra.coeff_single_apply {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {a a' : G} {b : k} [Decidable (a = a')] :

(single a b).coeff a' = if a = a' then b else 0

theorem SkewMonoidAlgebra.single_zero_right {k : Type u_1} {G : Type u_2} [AddCommMonoid k] (a : G) :

single a 0 = 0

@[simp]

theorem SkewMonoidAlgebra.single_add {k : Type u_1} {G : Type u_2} [AddCommMonoid k] (a : G) (b₁ b₂ : k) :

single a (b₁ + b₂) = single a b₁ + single a b₂

theorem SkewMonoidAlgebra.single_zero {k : Type u_1} {G : Type u_2} [AddCommMonoid k] (a : G) :

single a 0 = 0

theorem SkewMonoidAlgebra.single_eq_zero {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {a : G} {b : k} :

single a b = 0 ↔ b = 0

def SkewMonoidAlgebra.toFinsuppAddEquiv {k : Type u_1} {G : Type u_2} [AddCommMonoid k] :

SkewMonoidAlgebra k G ≃+ (G →₀ k)

Group isomorphism between SkewMonoidAlgebra k G and G →₀ k. This is an implementation detail, but it can be useful to transfer results from Finsupp to SkewMonoidAlgebra.

Equations

SkewMonoidAlgebra.toFinsuppAddEquiv = { toFun := SkewMonoidAlgebra.toFinsupp, invFun := SkewMonoidAlgebra.ofFinsupp, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

Instances For

@[simp]

theorem SkewMonoidAlgebra.toFinsuppAddEquiv_apply {k : Type u_1} {G : Type u_2} [AddCommMonoid k] (self : SkewMonoidAlgebra k G) :

toFinsuppAddEquiv self = self.toFinsupp

@[simp]

theorem SkewMonoidAlgebra.toFinsuppAddEquiv_symm_apply {k : Type u_1} {G : Type u_2} [AddCommMonoid k] (toFinsupp : G →₀ k) :

toFinsuppAddEquiv.symm toFinsupp = { toFinsupp := toFinsupp }

theorem SkewMonoidAlgebra.smul_single {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {S : Type u_3} [SMulZeroClass S k] (s : S) (a : G) (b : k) :

s • single a b = single a (s • b)

theorem SkewMonoidAlgebra.single_injective {k : Type u_1} {G : Type u_2} [AddCommMonoid k] (a : G) :

Function.Injective (single a)

theorem IsSMulRegular.skewMonoidAlgebra_iff {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {S : Type u_3} [Monoid S] [DistribMulAction S k] {a : S} [Nonempty G] :

IsSMulRegular k a ↔ IsSMulRegular (SkewMonoidAlgebra k G) a

instance SkewMonoidAlgebra.instOne {k : Type u_1} {G : Type u_2} [AddCommMonoid k] [One G] [One k] :

One (SkewMonoidAlgebra k G)

The unit of the multiplication is single 1 1, i.e. the function that is 1 at 1 and zero elsewhere.

Equations

SkewMonoidAlgebra.instOne = { one := SkewMonoidAlgebra.single 1 1 }

theorem SkewMonoidAlgebra.ofFinsupp_one {k : Type u_1} {G : Type u_2} [AddCommMonoid k] [One G] [One k] :

{ toFinsupp := Finsupp.single 1 1 } = 1

@[simp]

theorem SkewMonoidAlgebra.toFinsupp_one {k : Type u_1} {G : Type u_2} [AddCommMonoid k] [One G] [One k] :

toFinsupp 1 = Finsupp.single 1 1

@[simp]

theorem SkewMonoidAlgebra.toFinsupp_eq_single_one_one_iff {k : Type u_1} {G : Type u_2} [AddCommMonoid k] [One G] [One k] {a : SkewMonoidAlgebra k G} :

a.toFinsupp = Finsupp.single 1 1 ↔ a = 1

@[simp]

theorem SkewMonoidAlgebra.ofFinsupp_eq_one {k : Type u_1} {G : Type u_2} [AddCommMonoid k] [One G] [One k] {a : G →₀ k} :

{ toFinsupp := a } = 1 ↔ a = Finsupp.single 1 1

theorem SkewMonoidAlgebra.single_one_one {k : Type u_1} [AddCommMonoid k] [One k] :

single 1 1 = 1

theorem SkewMonoidAlgebra.one_def {k : Type u_1} {G : Type u_2} [AddCommMonoid k] [One G] [One k] :

1 = single 1 1

@[simp]

theorem SkewMonoidAlgebra.coeff_one_one {k : Type u_1} {G : Type u_2} [AddCommMonoid k] [One G] [One k] :

coeff 1 1 = 1

theorem SkewMonoidAlgebra.coeff_one {k : Type u_1} {G : Type u_2} [AddCommMonoid k] [One G] [One k] {a : G} [Decidable (a = 1)] :

coeff 1 a = if a = 1 then 1 else 0

instance SkewMonoidAlgebra.instDecidableEq {k : Type u_1} {G : Type u_2} [AddCommMonoid k] [DecidableEq G] [DecidableEq k] :

DecidableEq (SkewMonoidAlgebra k G)

Equations

SkewMonoidAlgebra.instDecidableEq = SkewMonoidAlgebra.toFinsuppAddEquiv.decidableEq

def SkewMonoidAlgebra.sum {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {N : Type u_3} [AddCommMonoid N] (f : SkewMonoidAlgebra k G) (g : G → k → N) :

N

sum f g is the sum of g a (f.coeff a) over the support of f.

Equations

f.sum g = f.toFinsupp.sum g

Instances For

theorem SkewMonoidAlgebra.sum_def {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {N : Type u_3} [AddCommMonoid N] (f : SkewMonoidAlgebra k G) (g : G → k → N) :

f.sum g = f.toFinsupp.sum g

theorem SkewMonoidAlgebra.sum_def' {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {N : Type u_3} [AddCommMonoid N] (f : SkewMonoidAlgebra k G) (g : G → k → N) :

f.sum g = ∑ a ∈ f.support, g a (f.coeff a)

Unfolded version of sum_def in terms of Finset.sum.

@[simp]

theorem SkewMonoidAlgebra.sum_single_index {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {N : Type u_3} [AddCommMonoid N] {a : G} {b : k} {h : G → k → N} (h_zero : h a 0 = 0) :

(single a b).sum h = h a b

theorem SkewMonoidAlgebra.map_sum {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {N : Type u_3} {P : Type u_4} [AddCommMonoid N] [AddCommMonoid P] {H : Type u_5} [FunLike H N P] [AddMonoidHomClass H N P] (h : H) (f : SkewMonoidAlgebra k G) (g : G → k → N) :

h (f.sum g) = f.sum fun (a : G) (b : k) => h (g a b)

theorem SkewMonoidAlgebra.toFinsupp_sum' {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {k' : Type u_3} {G' : Type u_4} [AddCommMonoid k'] (f : SkewMonoidAlgebra k G) (g : G → k → SkewMonoidAlgebra k' G') :

(f.sum g).toFinsupp = f.toFinsupp.sum fun (x1 : G) (x2 : k) => (g x1 x2).toFinsupp

Variant where the image of g is a SkewMonoidAlgebra.

theorem SkewMonoidAlgebra.ofFinsupp_sum {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {k' : Type u_3} {G' : Type u_4} [AddCommMonoid k'] (f : G →₀ k) (g : G → k → G' →₀ k') :

{ toFinsupp := f.sum g } = { toFinsupp := f }.sum fun (x1 : G) (x2 : k) => { toFinsupp := g x1 x2 }

theorem SkewMonoidAlgebra.sum_single {k : Type u_1} {G : Type u_2} [AddCommMonoid k] (f : SkewMonoidAlgebra k G) :

f.sum single = f

theorem SkewMonoidAlgebra.sum_add_index' {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {S : Type u_3} [AddCommMonoid S] {f g : SkewMonoidAlgebra k G} {h : G → k → S} (hf : ∀ (i : G), h i 0 = 0) (h_add : ∀ (a : G) (b₁ b₂ : k), h a (b₁ + b₂) = h a b₁ + h a b₂) :

(f + g).sum h = f.sum h + g.sum h

Taking the sum under h is an additive homomorphism, if h is an additive homomorphism. This is a more specific version of SkewMonoidAlgebra.sum_add_index with simpler hypotheses.

theorem SkewMonoidAlgebra.sum_add_index {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {S : Type u_3} [DecidableEq G] [AddCommMonoid S] {f g : SkewMonoidAlgebra k G} {h : G → k → S} (h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 0) (h_add : ∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂ : k), h a (b₁ + b₂) = h a b₁ + h a b₂) :

(f + g).sum h = f.sum h + g.sum h

Taking the sum under h is an additive homomorphism, if h is an additive homomorphism. This is a more general version of SkewMonoidAlgebra.sum_add_index'; the latter has simpler hypotheses.

@[simp]

theorem SkewMonoidAlgebra.sum_add {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {S : Type u_3} [AddCommMonoid S] (p : SkewMonoidAlgebra k G) (f g : G → k → S) :

(p.sum fun (n : G) (x : k) => f n x + g n x) = p.sum f + p.sum g

@[simp]

theorem SkewMonoidAlgebra.sum_zero_index {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {S : Type u_3} [AddCommMonoid S] {f : G → k → S} :

sum 0 f = 0

@[simp]

theorem SkewMonoidAlgebra.sum_zero {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {N : Type u_3} [AddCommMonoid N] {f : SkewMonoidAlgebra k G} :

(f.sum fun (x : G) (x : k) => 0) = 0

theorem SkewMonoidAlgebra.sum_sum_index {α : Type u_3} {β : Type u_4} {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] {f : SkewMonoidAlgebra M α} {g : α → M → SkewMonoidAlgebra N β} {h : β → N → P} (h_zero : ∀ (a : β), h a 0 = 0) (h_add : ∀ (a : β) (b₁ b₂ : N), h a (b₁ + b₂) = h a b₁ + h a b₂) :

(f.sum g).sum h = f.sum fun (a : α) (b : M) => (g a b).sum h

@[simp]

theorem SkewMonoidAlgebra.coeff_sum {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {k' : Type u_3} {G' : Type u_4} [AddCommMonoid k'] {f : SkewMonoidAlgebra k G} {g : G → k → SkewMonoidAlgebra k' G'} {a₂ : G'} :

(f.sum g).coeff a₂ = f.sum fun (a₁ : G) (b : k) => (g a₁ b).coeff a₂

theorem SkewMonoidAlgebra.sum_mul {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {S : Type u_3} [NonUnitalNonAssocSemiring S] (b : S) (s : SkewMonoidAlgebra k G) {f : G → k → S} :

s.sum f * b = s.sum fun (a : G) (c : k) => f a c * b

theorem SkewMonoidAlgebra.mul_sum {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {S : Type u_3} [NonUnitalNonAssocSemiring S] (b : S) (s : SkewMonoidAlgebra k G) {f : G → k → S} :

b * s.sum f = s.sum fun (a : G) (c : k) => b * f a c

@[simp]

theorem SkewMonoidAlgebra.sum_ite_eq' {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {N : Type u_3} [AddCommMonoid N] [DecidableEq G] (f : SkewMonoidAlgebra k G) (a : G) (b : G → k → N) :

(f.sum fun (x : G) (v : k) => if x = a then b x v else 0) = if a ∈ f.support then b a (f.coeff a) else 0

Analogue of Finsupp.sum_ite_eq' for SkewMonoidAlgebra.

theorem SkewMonoidAlgebra.smul_sum {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {M : Type u_3} {R : Type u_4} [AddCommMonoid M] [DistribSMul R M] {v : SkewMonoidAlgebra k G} {c : R} {h : G → k → M} :

c • v.sum h = v.sum fun (a : G) (b : k) => c • h a b

theorem SkewMonoidAlgebra.sum_congr {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {f : SkewMonoidAlgebra k G} {M : Type u_3} [AddCommMonoid M] {g₁ g₂ : G → k → M} (h : ∀ x ∈ f.support, g₁ x (f.coeff x) = g₂ x (f.coeff x)) :

f.sum g₁ = f.sum g₂