# mathlibdocumentation

data.finsupp.pointwise

# The pointwise product on finsupp.

TODO per issue #1864: We intend to remove the convolution product on finsupp, and define it only on a type synonym add_monoid_algebra. After we've done this, it would be good to make this the default product on finsupp.

### Declarations about the pointwise product on finsupps

@[instance]
def finsupp.has_mul {α : Type u₁} {β : Type u₂}  :
has_mul →₀ β)

The product of f g : α →₀ β is the finitely supported function whose value at a is f a * g a.

Equations
@[simp]
theorem finsupp.mul_apply {α : Type u₁} {β : Type u₂} {g₁ g₂ : α →₀ β} {a : α} :
(g₁ * g₂) a = (g₁ a) * g₂ a

theorem finsupp.support_mul {α : Type u₁} {β : Type u₂} {g₁ g₂ : α →₀ β} :
(g₁ * g₂).support g₁.support g₂.support

@[instance]
def finsupp.semigroup {α : Type u₁} {β : Type u₂} [semiring β] :

Equations
@[instance]
def finsupp.distrib {α : Type u₁} {β : Type u₂} [semiring β] :
distrib →₀ β)

Equations