# 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.instMul {α : Type u₁} {β : Type u₂} [] :
Mul (α →₀ β)

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

Equations
theorem Finsupp.coe_mul {α : Type u₁} {β : Type u₂} [] (g₁ : α →₀ β) (g₂ : α →₀ β) :
(g₁ * g₂) = g₁ * g₂
@[simp]
theorem Finsupp.mul_apply {α : Type u₁} {β : Type u₂} [] {g₁ : α →₀ β} {g₂ : α →₀ β} {a : α} :
(g₁ * g₂) a = g₁ a * g₂ a
@[simp]
theorem Finsupp.single_mul {α : Type u₁} {β : Type u₂} [] (a : α) (b₁ : β) (b₂ : β) :
Finsupp.single a (b₁ * b₂) = *
theorem Finsupp.support_mul {α : Type u₁} {β : Type u₂} [] [] {g₁ : α →₀ β} {g₂ : α →₀ β} :
(g₁ * g₂).support g₁.support g₂.support
instance Finsupp.instMulZeroClass {α : Type u₁} {β : Type u₂} [] :
Equations
instance Finsupp.instSemigroupWithZero {α : Type u₁} {β : Type u₂} :
Equations
instance Finsupp.instNonUnitalNonAssocSemiring {α : Type u₁} {β : Type u₂} :
Equations
instance Finsupp.instNonUnitalSemiring {α : Type u₁} {β : Type u₂} :
Equations
instance Finsupp.instNonUnitalCommSemiring {α : Type u₁} {β : Type u₂} :
Equations
instance Finsupp.instNonUnitalNonAssocRing {α : Type u₁} {β : Type u₂} :
Equations
instance Finsupp.instNonUnitalRing {α : Type u₁} {β : Type u₂} [] :
Equations
instance Finsupp.instNonUnitalCommRing {α : Type u₁} {β : Type u₂} :
Equations
instance Finsupp.pointwiseScalar {α : Type u₁} {β : Type u₂} [] :
SMul (αβ) (α →₀ β)
Equations
@[simp]
theorem Finsupp.coe_pointwise_smul {α : Type u₁} {β : Type u₂} [] (f : αβ) (g : α →₀ β) :
(f g) = f g
instance Finsupp.pointwiseModule {α : Type u₁} {β : Type u₂} [] :
Module (αβ) (α →₀ β)

The pointwise multiplicative action of functions on finitely supported functions

Equations