mathlib documentation


The pointwise product on finsupp. #

For the convolution product on finsupp when the domain has a binary operation, see the type synonyms add_monoid_algebra (which is in turn used to define polynomial and mv_polynomial) and monoid_algebra.

Declarations about the pointwise product on finsupps #

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

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

theorem finsupp.mul_apply {α : Type u₁} {β : Type u₂} [mul_zero_class β] {g₁ g₂ : α →₀ β} {a : α} :
(g₁ * g₂) a = (g₁ a) * g₂ a
theorem finsupp.support_mul {α : Type u₁} {β : Type u₂} [mul_zero_class β] {g₁ g₂ : α →₀ β} :
(g₁ * g₂).support g₁.support g₂.support
def finsupp.mul_zero_class {α : Type u₁} {β : Type u₂} [mul_zero_class β] :