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 #

source
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) (_ : 0 * 0 = 0) }
source
theorem Finsupp.coe_mul {α : Type u₁} {β : Type u₂} [MulZeroClass β] (g₁ : α →₀ β) (g₂ : α →₀ β) :
⇑(g₁ * g₂) = ⇑g₁ * ⇑g₂
source
@[simp]
theorem Finsupp.mul_apply {α : Type u₁} {β : Type u₂} [MulZeroClass β] {g₁ : α →₀ β} {g₂ : α →₀ β} {a : α} :
(g₁ * g₂) a = g₁ a * g₂ a
source
@[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₂
source
theorem Finsupp.support_mul {α : Type u₁} {β : Type u₂} [MulZeroClass β] [DecidableEq α] {g₁ : α →₀ β} {g₂ : α →₀ β} :
(g₁ * g₂).support ⊆ g₁.support ∩ g₂.support
source
instance Finsupp.instMulZeroClassFinsuppToZero {α : Type u₁} {β : Type u₂} [MulZeroClass β] :
MulZeroClass (α →₀ β)
Equations
  • One or more equations did not get rendered due to their size.
source
instance Finsupp.instSemigroupWithZeroFinsuppToZero {α : Type u₁} {β : Type u₂} [SemigroupWithZero β] :
SemigroupWithZero (α →₀ β)
Equations
  • One or more equations did not get rendered due to their size.
source
instance Finsupp.instNonUnitalNonAssocSemiringFinsuppToZeroToMulZeroClass {α : Type u₁} {β : Type u₂} [NonUnitalNonAssocSemiring β] :
NonUnitalNonAssocSemiring (α →₀ β)
Equations
  • One or more equations did not get rendered due to their size.
source
instance Finsupp.instNonUnitalSemiringFinsuppToZeroToSemigroupWithZero {α : Type u₁} {β : Type u₂} [NonUnitalSemiring β] :
NonUnitalSemiring (α →₀ β)
Equations
  • One or more equations did not get rendered due to their size.
source
instance Finsupp.instNonUnitalCommSemiringFinsuppToZeroToSemigroupWithZeroToNonUnitalSemiring {α : Type u₁} {β : Type u₂} [NonUnitalCommSemiring β] :
NonUnitalCommSemiring (α →₀ β)
Equations
  • One or more equations did not get rendered due to their size.
source
instance Finsupp.instNonUnitalNonAssocRingFinsuppToZeroToMulZeroClassToNonUnitalNonAssocSemiring {α : Type u₁} {β : Type u₂} [NonUnitalNonAssocRing β] :
NonUnitalNonAssocRing (α →₀ β)
Equations
  • One or more equations did not get rendered due to their size.
source
instance Finsupp.instNonUnitalRingFinsuppToZeroToSemigroupWithZeroToNonUnitalSemiring {α : Type u₁} {β : Type u₂} [NonUnitalRing β] :
NonUnitalRing (α →₀ β)
Equations
  • One or more equations did not get rendered due to their size.
source
instance Finsupp.instNonUnitalCommRingFinsuppToZeroToSemigroupWithZeroToNonUnitalSemiringToNonUnitalCommSemiring {α : Type u₁} {β : Type u₂} [NonUnitalCommRing β] :
NonUnitalCommRing (α →₀ β)
Equations
  • One or more equations did not get rendered due to their size.
source
instance Finsupp.pointwiseScalar {α : Type u₁} {β : Type u₂} [Semiring β] :
SMul (α → β) (α →₀ β)
Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem Finsupp.coe_pointwise_smul {α : Type u₁} {β : Type u₂} [Semiring β] (f : α → β) (g : α →₀ β) :
⇑(f • g) = f • ⇑g
source
instance Finsupp.pointwiseModule {α : Type u₁} {β : Type u₂} [Semiring β] :
Module (α → β) (α →₀ β)

The pointwise multiplicative action of functions on finitely supported functions

Equations