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
.
Equations
- Finsupp.instMulFinsuppToZero = { mul := Finsupp.zipWith (fun x x_1 => x * x_1) (_ : 0 * 0 = 0) }
theorem
Finsupp.support_mul
{α : Type u₁}
{β : Type u₂}
[inst : MulZeroClass β]
[inst : DecidableEq α]
{g₁ : α →₀ β}
{g₂ : α →₀ β}
:
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₂)
instance
Finsupp.instSemigroupWithZeroFinsuppToZero
{α : Type u₁}
{β : Type u₂}
[inst : SemigroupWithZero β]
:
SemigroupWithZero (α →₀ β)
Equations
- One or more equations did not get rendered due to their size.
instance
Finsupp.instNonUnitalNonAssocSemiringFinsuppToZeroToMulZeroClass
{α : Type u₁}
{β : Type u₂}
[inst : NonUnitalNonAssocSemiring β]
:
NonUnitalNonAssocSemiring (α →₀ β)
Equations
- One or more equations did not get rendered due to their size.
instance
Finsupp.instNonUnitalSemiringFinsuppToZeroToSemigroupWithZero
{α : Type u₁}
{β : Type u₂}
[inst : NonUnitalSemiring β]
:
NonUnitalSemiring (α →₀ β)
Equations
- One or more equations did not get rendered due to their size.
instance
Finsupp.instNonUnitalCommSemiringFinsuppToZeroToSemigroupWithZeroToNonUnitalSemiring
{α : Type u₁}
{β : Type u₂}
[inst : NonUnitalCommSemiring β]
:
NonUnitalCommSemiring (α →₀ β)
Equations
- One or more equations did not get rendered due to their size.
instance
Finsupp.instNonUnitalNonAssocRingFinsuppToZeroToMulZeroClassToNonUnitalNonAssocSemiring
{α : Type u₁}
{β : Type u₂}
[inst : NonUnitalNonAssocRing β]
:
NonUnitalNonAssocRing (α →₀ β)
Equations
- One or more equations did not get rendered due to their size.
instance
Finsupp.instNonUnitalRingFinsuppToZeroToSemigroupWithZeroToNonUnitalSemiring
{α : Type u₁}
{β : Type u₂}
[inst : NonUnitalRing β]
:
NonUnitalRing (α →₀ β)
Equations
- One or more equations did not get rendered due to their size.
instance
Finsupp.instNonUnitalCommRingFinsuppToZeroToSemigroupWithZeroToNonUnitalSemiringToNonUnitalRing
{α : Type u₁}
{β : Type u₂}
[inst : NonUnitalCommRing β]
:
NonUnitalCommRing (α →₀ β)
Equations
- One or more equations did not get rendered due to their size.
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)) }
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))