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
.
The product of f g : α →₀ β
is the finitely supported function
whose value at a
is f a * g a
.
@[simp]
theorem
Finsupp.mul_apply
{α : Type u₁}
{β : Type u₂}
[MulZeroClass β]
{g₁ : α →₀ β}
{g₂ : α →₀ β}
{a : α}
:
theorem
Finsupp.support_mul
{α : Type u₁}
{β : Type u₂}
[MulZeroClass β]
[DecidableEq α]
{g₁ : α →₀ β}
{g₂ : α →₀ β}
:
instance
Finsupp.instMulZeroClassFinsuppToZero
{α : Type u₁}
{β : Type u₂}
[MulZeroClass β]
:
MulZeroClass (α →₀ β)
instance
Finsupp.instSemigroupWithZeroFinsuppToZero
{α : Type u₁}
{β : Type u₂}
[SemigroupWithZero β]
:
SemigroupWithZero (α →₀ β)
instance
Finsupp.instNonUnitalNonAssocSemiringFinsuppToZeroToMulZeroClass
{α : Type u₁}
{β : Type u₂}
[NonUnitalNonAssocSemiring β]
:
NonUnitalNonAssocSemiring (α →₀ β)
instance
Finsupp.instNonUnitalSemiringFinsuppToZeroToSemigroupWithZero
{α : Type u₁}
{β : Type u₂}
[NonUnitalSemiring β]
:
NonUnitalSemiring (α →₀ β)
instance
Finsupp.instNonUnitalCommSemiringFinsuppToZeroToSemigroupWithZeroToNonUnitalSemiring
{α : Type u₁}
{β : Type u₂}
[NonUnitalCommSemiring β]
:
NonUnitalCommSemiring (α →₀ β)
instance
Finsupp.instNonUnitalNonAssocRingFinsuppToZeroToMulZeroClassToNonUnitalNonAssocSemiring
{α : Type u₁}
{β : Type u₂}
[NonUnitalNonAssocRing β]
:
NonUnitalNonAssocRing (α →₀ β)
instance
Finsupp.instNonUnitalRingFinsuppToZeroToSemigroupWithZeroToNonUnitalSemiring
{α : Type u₁}
{β : Type u₂}
[NonUnitalRing β]
:
NonUnitalRing (α →₀ β)
instance
Finsupp.instNonUnitalCommRingFinsuppToZeroToSemigroupWithZeroToNonUnitalSemiringToNonUnitalCommSemiring
{α : Type u₁}
{β : Type u₂}
[NonUnitalCommRing β]
:
NonUnitalCommRing (α →₀ β)