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₂} [MulZeroClass β] :
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) }
theorem Finsupp.coe_mul {α : Type u₁} {β : Type u₂} [MulZeroClass β] (g₁ : α →₀ β) (g₂ : α →₀ β) :
(g₁ * g₂) = g₁ * g₂
@[simp]
theorem Finsupp.mul_apply {α : Type u₁} {β : Type u₂} [MulZeroClass β] {g₁ : α →₀ β} {g₂ : α →₀ β} {a : α} :
(g₁ * g₂) a = g₁ a * g₂ a
@[simp]
theorem Finsupp.single_mul {α : Type u₁} {β : Type u₂} [MulZeroClass β] (a : α) (b₁ : β) (b₂ : β) :
Finsupp.single a (b₁ * b₂) = Finsupp.single a b₁ * Finsupp.single a b₂
theorem Finsupp.support_mul {α : Type u₁} {β : Type u₂} [MulZeroClass β] [DecidableEq α] {g₁ : α →₀ β} {g₂ : α →₀ β} :
(g₁ * g₂).support g₁.support g₂.support
instance Finsupp.instMulZeroClassFinsuppToZero {α : Type u₁} {β : Type u₂} [MulZeroClass β] :
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
instance Finsupp.pointwiseScalar {α : Type u₁} {β : Type u₂} [Semiring β] :
SMul (αβ) (α →₀ β)
Equations
@[simp]
theorem Finsupp.coe_pointwise_smul {α : Type u₁} {β : Type u₂} [Semiring β] (f : αβ) (g : α →₀ β) :
(f g) = f g
instance Finsupp.pointwiseModule {α : Type u₁} {β : Type u₂} [Semiring β] :
Module (αβ) (α →₀ β)

The pointwise multiplicative action of functions on finitely supported functions

Equations