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

def Finsupp.instMul {α : Type u₁} {β : Type u₂} [MulZeroClass β] : Mul (Finsupp α β)

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

Equations

• Eq Finsupp.instMul { mul := Finsupp.zipWith (fun (x1 x2 : β) => HMul.hMul x1 x2) ⋯ }

theorem Finsupp.coe_mul {α : Type u₁} {β : Type u₂} [MulZeroClass β] (g₁ g₂ : Finsupp α β) : Eq (DFunLike.coe (HMul.hMul g₁ g₂)) (HMul.hMul (DFunLike.coe g₁) (DFunLike.coe g₂))

theorem Finsupp.mul_apply {α : Type u₁} {β : Type u₂} [MulZeroClass β] {g₁ g₂ : Finsupp α β} {a : α} : Eq (DFunLike.coe (HMul.hMul g₁ g₂) a) (HMul.hMul (DFunLike.coe g₁ a) (DFunLike.coe g₂ a))

theorem Finsupp.single_mul {α : Type u₁} {β : Type u₂} [MulZeroClass β] (a : α) (b₁ b₂ : β) : Eq (single a (HMul.hMul b₁ b₂)) (HMul.hMul (single a b₁) (single a b₂))

theorem Finsupp.support_mul_subset_left {α : Type u₁} {β : Type u₂} [MulZeroClass β] {g₁ g₂ : Finsupp α β} : HasSubset.Subset (HMul.hMul g₁ g₂).support g₁.support

theorem Finsupp.support_mul_subset_right {α : Type u₁} {β : Type u₂} [MulZeroClass β] {g₁ g₂ : Finsupp α β} : HasSubset.Subset (HMul.hMul g₁ g₂).support g₂.support

theorem Finsupp.support_mul {α : Type u₁} {β : Type u₂} [MulZeroClass β] [DecidableEq α] {g₁ g₂ : Finsupp α β} : HasSubset.Subset (HMul.hMul g₁ g₂).support (Inter.inter g₁.support g₂.support)

def Finsupp.instMulZeroClass {α : Type u₁} {β : Type u₂} [MulZeroClass β] : MulZeroClass (Finsupp α β)

Equations

• Eq Finsupp.instMulZeroClass (Function.Injective.mulZeroClass (fun (f : Finsupp α β) => DFunLike.coe f) ⋯ ⋯ ⋯)

def Finsupp.instSemigroupWithZero {α : Type u₁} {β : Type u₂} [SemigroupWithZero β] : SemigroupWithZero (Finsupp α β)

Equations

• Eq Finsupp.instSemigroupWithZero (Function.Injective.semigroupWithZero (fun (f : Finsupp α β) => DFunLike.coe f) ⋯ ⋯ ⋯)

def Finsupp.instNonUnitalNonAssocSemiring {α : Type u₁} {β : Type u₂} [NonUnitalNonAssocSemiring β] : NonUnitalNonAssocSemiring (Finsupp α β)

Equations

• Eq Finsupp.instNonUnitalNonAssocSemiring (Function.Injective.nonUnitalNonAssocSemiring (fun (f : Finsupp α β) => DFunLike.coe f) ⋯ ⋯ ⋯ ⋯ ⋯)

def Finsupp.instNonUnitalSemiring {α : Type u₁} {β : Type u₂} [NonUnitalSemiring β] : NonUnitalSemiring (Finsupp α β)

Equations

• Eq Finsupp.instNonUnitalSemiring (Function.Injective.nonUnitalSemiring (fun (f : Finsupp α β) => DFunLike.coe f) ⋯ ⋯ ⋯ ⋯ ⋯)

def Finsupp.instNonUnitalCommSemiring {α : Type u₁} {β : Type u₂} [NonUnitalCommSemiring β] : NonUnitalCommSemiring (Finsupp α β)

Equations

• Eq Finsupp.instNonUnitalCommSemiring (Function.Injective.nonUnitalCommSemiring (fun (f : Finsupp α β) => DFunLike.coe f) ⋯ ⋯ ⋯ ⋯ ⋯)

def Finsupp.instNonUnitalNonAssocRing {α : Type u₁} {β : Type u₂} [NonUnitalNonAssocRing β] : NonUnitalNonAssocRing (Finsupp α β)

Equations

• Eq Finsupp.instNonUnitalNonAssocRing (Function.Injective.nonUnitalNonAssocRing (fun (f : Finsupp α β) => DFunLike.coe f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯)

def Finsupp.instNonUnitalRing {α : Type u₁} {β : Type u₂} [NonUnitalRing β] : NonUnitalRing (Finsupp α β)

Equations

• Eq Finsupp.instNonUnitalRing (Function.Injective.nonUnitalRing (fun (f : Finsupp α β) => DFunLike.coe f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯)

def Finsupp.instNonUnitalCommRing {α : Type u₁} {β : Type u₂} [NonUnitalCommRing β] : NonUnitalCommRing (Finsupp α β)

Equations

• Eq Finsupp.instNonUnitalCommRing (Function.Injective.nonUnitalCommRing (fun (f : Finsupp α β) => DFunLike.coe f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯)

def Finsupp.pointwiseScalar {α : Type u₁} {β : Type u₂} [Semiring β] : SMul (α → β) (Finsupp α β)

Equations

• Eq Finsupp.pointwiseScalar { smul := fun (f : α → β) (g : Finsupp α β) => Finsupp.ofSupportFinite (fun (a : α) => HSMul.hSMul (f a) (DFunLike.coe g a)) ⋯ }

theorem Finsupp.coe_pointwise_smul {α : Type u₁} {β : Type u₂} [Semiring β] (f : α → β) (g : Finsupp α β) : Eq (DFunLike.coe (HSMul.hSMul f g)) (HSMul.hSMul f (DFunLike.coe g))

def Finsupp.pointwiseModule {α : Type u₁} {β : Type u₂} [Semiring β] : Module (α → β) (Finsupp α β)

The pointwise multiplicative action of functions on finitely supported functions

Equations

• Eq Finsupp.pointwiseModule (Function.Injective.module (α → β) Finsupp.coeFnAddHom ⋯ ⋯)