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_reducible]

noncomputable instance Finsupp.instMul {α : 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.instMul = { mul := Finsupp.zipWith (fun (x1 x2 : β) => x1 * x2) ⋯ }

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₂ : β) : single a (b₁ * b₂) = single a b₁ * single a b₂

theorem Finsupp.support_mul_subset_left {α : Type u₁} {β : Type u₂} [MulZeroClass β] {g₁ g₂ : α →₀ β} : (g₁ * g₂).support ⊆ g₁.support

theorem Finsupp.support_mul_subset_right {α : Type u₁} {β : Type u₂} [MulZeroClass β] {g₁ g₂ : α →₀ β} : (g₁ * g₂).support ⊆ g₂.support

theorem Finsupp.support_mul {α : Type u₁} {β : Type u₂} [MulZeroClass β] [DecidableEq α] {g₁ g₂ : α →₀ β} : (g₁ * g₂).support ⊆ g₁.support ∩ g₂.support

@[instance_reducible]

noncomputable instance Finsupp.instMulZeroClass {α : Type u₁} {β : Type u₂} [MulZeroClass β] : MulZeroClass (α →₀ β)

Equations

• Finsupp.instMulZeroClass = Function.Injective.mulZeroClass DFunLike.coe ⋯ ⋯ ⋯

@[instance_reducible]

noncomputable instance Finsupp.instSemigroupWithZero {α : Type u₁} {β : Type u₂} [SemigroupWithZero β] : SemigroupWithZero (α →₀ β)

Equations

• Finsupp.instSemigroupWithZero = Function.Injective.semigroupWithZero DFunLike.coe ⋯ ⋯ ⋯

@[instance_reducible]

noncomputable instance Finsupp.instNonUnitalNonAssocSemiring {α : Type u₁} {β : Type u₂} [NonUnitalNonAssocSemiring β] : NonUnitalNonAssocSemiring (α →₀ β)

Equations

• Finsupp.instNonUnitalNonAssocSemiring = Function.Injective.nonUnitalNonAssocSemiring DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯

@[instance_reducible]

noncomputable instance Finsupp.instNonUnitalSemiring {α : Type u₁} {β : Type u₂} [NonUnitalSemiring β] : NonUnitalSemiring (α →₀ β)

Equations

• Finsupp.instNonUnitalSemiring = Function.Injective.nonUnitalSemiring DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯

@[instance_reducible]

noncomputable instance Finsupp.instNonUnitalCommSemiring {α : Type u₁} {β : Type u₂} [NonUnitalCommSemiring β] : NonUnitalCommSemiring (α →₀ β)

Equations

• Finsupp.instNonUnitalCommSemiring = Function.Injective.nonUnitalCommSemiring DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯

@[instance_reducible]

noncomputable instance Finsupp.instNonUnitalNonAssocRing {α : Type u₁} {β : Type u₂} [NonUnitalNonAssocRing β] : NonUnitalNonAssocRing (α →₀ β)

Equations

• Finsupp.instNonUnitalNonAssocRing = Function.Injective.nonUnitalNonAssocRing DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[instance_reducible]

noncomputable instance Finsupp.instNonUnitalRing {α : Type u₁} {β : Type u₂} [NonUnitalRing β] : NonUnitalRing (α →₀ β)

Equations

• Finsupp.instNonUnitalRing = Function.Injective.nonUnitalRing DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[instance_reducible]

noncomputable instance Finsupp.instNonUnitalCommRing {α : Type u₁} {β : Type u₂} [NonUnitalCommRing β] : NonUnitalCommRing (α →₀ β)

Equations

• Finsupp.instNonUnitalCommRing = Function.Injective.nonUnitalCommRing DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

theorem Finsupp.pointwise_smul_support_finite {α : Type u₁} {β : Type u₂} {γ : Type u₃} [Zero γ] [SMulZeroClass β γ] (f : α → β) (g : α →₀ γ) : (Function.support fun (x : α) => f x • g x).Finite

@[reducible, inline]

noncomputable abbrev Finsupp.pointwiseScalar {α : Type u₁} {β : Type u₂} {γ : Type u₃} [Zero γ] [SMulZeroClass β γ] : SMul (α → β) (α →₀ γ)

Pointwise scalar multiplication given by (f • g) x = f x • g x.

Equations

• Finsupp.pointwiseScalar = { smul := fun (f : α → β) (g : α →₀ γ) => Finsupp.ofSupportFinite (fun (a : α) => f a • g a) ⋯ }

@[instance_reducible]

noncomputable instance Finsupp.pointwiseScalarSemiring {α : Type u₁} {β : Type u₂} [Semiring β] : SMul (α → β) (α →₀ β)

Equations

• Finsupp.pointwiseScalarSemiring = Finsupp.pointwiseScalar

@[simp]

theorem Finsupp.coe_pointwise_smul {α : Type u₁} {β : Type u₂} [Semiring β] (f : α → β) (g : α →₀ β) : ⇑(f • g) = f • ⇑g

@[instance_reducible]

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

The pointwise multiplicative action of functions on finitely supported functions

Equations

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

instance Finsupp.instIsScalarTowerForall {α : Type u₁} {β : Type u₂} [Semiring β] : IsScalarTower β (α → β) (α →₀ β)