# Documentation

Mathlib.Data.Finsupp.Pointwise

# The pointwise product on Finsupp. #

For the convolution product on Finsupp when the domain has a binary operation, see the type synonyms AddMonoidAlgebra (which is in turn used to define Polynomial and MvPolynomial) and MonoidAlgebra.

### Declarations about the pointwise product on Finsupps #

instance Finsupp.instMulFinsuppToZero {α : Type u₁} {β : Type u₂} [inst : ] :
Mul (α →₀ β)

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

Equations
• Finsupp.instMulFinsuppToZero = { mul := Finsupp.zipWith (fun x x_1 => x * x_1) (_ : 0 * 0 = 0) }
theorem Finsupp.coe_mul {α : Type u₁} {β : Type u₂} [inst : ] (g₁ : α →₀ β) (g₂ : α →₀ β) :
↑(g₁ * g₂) = g₁ * g₂
@[simp]
theorem Finsupp.mul_apply {α : Type u₁} {β : Type u₂} [inst : ] {g₁ : α →₀ β} {g₂ : α →₀ β} {a : α} :
↑(g₁ * g₂) a = g₁ a * g₂ a
theorem Finsupp.support_mul {α : Type u₁} {β : Type u₂} [inst : ] [inst : ] {g₁ : α →₀ β} {g₂ : α →₀ β} :
(g₁ * g₂).support g₁.support g₂.support
instance Finsupp.instMulZeroClassFinsuppToZero {α : Type u₁} {β : Type u₂} [inst : ] :
Equations
instance Finsupp.instSemigroupWithZeroFinsuppToZero {α : Type u₁} {β : Type u₂} [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
instance Finsupp.pointwiseScalar {α : Type u₁} {β : Type u₂} [inst : ] :
SMul (αβ) (α →₀ β)
Equations
@[simp]
theorem Finsupp.coe_pointwise_smul {α : Type u₁} {β : Type u₂} [inst : ] (f : αβ) (g : α →₀ β) :
↑(f g) = ↑(f g)
instance Finsupp.pointwiseModule {α : Type u₁} {β : Type u₂} [inst : ] :
Module (αβ) (α →₀ β)

The pointwise multiplicative action of functions on finitely supported functions

Equations