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

ink

instance Finsupp.instMulFinsuppToZero {α : Type u₁} {β : Type u₂} [inst : 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) }

ink

theorem Finsupp.coe_mul {α : Type u₁} {β : Type u₂} [inst : MulZeroClass β] (g₁ : α →₀ β) (g₂ : α →₀ β) : ↑(g₁ * g₂) = ↑g₁ * ↑g₂

ink

@[simp]

theorem Finsupp.mul_apply {α : Type u₁} {β : Type u₂} [inst : MulZeroClass β] {g₁ : α →₀ β} {g₂ : α →₀ β} {a : α} : ↑(g₁ * g₂) a = ↑g₁ a * ↑g₂ a

ink

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

ink

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

Equations

• Finsupp.instMulZeroClassFinsuppToZero = Function.Injective.mulZeroClass (fun f => ↑f) (_ : Function.Injective fun f => ↑f) (_ : ↑0 = 0) (_ : ∀ (g₁ g₂ : α →₀ β), ↑(g₁ * g₂) = ↑g₁ * ↑g₂)

ink

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

Equations

• One or more equations did not get rendered due to their size.

ink

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

Equations

• One or more equations did not get rendered due to their size.

ink

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

Equations

• One or more equations did not get rendered due to their size.

ink

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

Equations

• One or more equations did not get rendered due to their size.

ink

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

Equations

• One or more equations did not get rendered due to their size.

ink

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

Equations

• One or more equations did not get rendered due to their size.

ink

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

Equations

• One or more equations did not get rendered due to their size.

ink

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

Equations

• Finsupp.pointwiseScalar = { smul := fun f g => Finsupp.ofSupportFinite (fun a => f a • ↑g a) (_ : Set.Finite (Function.support fun a => f a • ↑g a)) }

ink

@[simp]

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

ink

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

The pointwise multiplicative action of functions on finitely supported functions

Equations

• Finsupp.pointwiseModule = Function.Injective.module (α → β) Finsupp.coeFnAddHom (_ : Function.Injective fun f => ↑f) (_ : ∀ (f : α → β) (g : α →₀ β), ↑(f • g) = ↑(f • g))