Documentation

Mathlib.Data.Finsupp.Pointwise

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 #

source
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
    source
    theorem Finsupp.coe_mul {α : Type u₁} {β : Type u₂} [MulZeroClass β] (g₁ g₂ : α →₀ β) :
    ⇑(g₁ * g₂) = ⇑g₁ * ⇑g₂
    source
    @[simp]
    theorem Finsupp.mul_apply {α : Type u₁} {β : Type u₂} [MulZeroClass β] {g₁ g₂ : α →₀ β} {a : α} :
    (g₁ * g₂) a = g₁ a * g₂ a
    source
    @[simp]
    theorem Finsupp.single_mul {α : Type u₁} {β : Type u₂} [MulZeroClass β] (a : α) (b₁ b₂ : β) :
    single a (b₁ * b₂) = single a b₁ * single a b₂
    source
    theorem Finsupp.support_mul_subset_left {α : Type u₁} {β : Type u₂} [MulZeroClass β] {g₁ g₂ : α →₀ β} :
    (g₁ * g₂).support ⊆ g₁.support
    source
    theorem Finsupp.support_mul_subset_right {α : Type u₁} {β : Type u₂} [MulZeroClass β] {g₁ g₂ : α →₀ β} :
    (g₁ * g₂).support ⊆ g₂.support
    source
    theorem Finsupp.support_mul {α : Type u₁} {β : Type u₂} [MulZeroClass β] [DecidableEq α] {g₁ g₂ : α →₀ β} :
    (g₁ * g₂).support ⊆ g₁.support ∩ g₂.support
    source
    instance Finsupp.instMulZeroClass {α : Type u₁} {β : Type u₂} [MulZeroClass β] :
    MulZeroClass (α →₀ β)
    Equations
      source
      instance Finsupp.instSemigroupWithZero {α : Type u₁} {β : Type u₂} [SemigroupWithZero β] :
      SemigroupWithZero (α →₀ β)
      Equations
        source
        instance Finsupp.instNonUnitalNonAssocSemiring {α : Type u₁} {β : Type u₂} [NonUnitalNonAssocSemiring β] :
        NonUnitalNonAssocSemiring (α →₀ β)
        Equations
          source
          instance Finsupp.instNonUnitalSemiring {α : Type u₁} {β : Type u₂} [NonUnitalSemiring β] :
          NonUnitalSemiring (α →₀ β)
          Equations
            source
            instance Finsupp.instNonUnitalCommSemiring {α : Type u₁} {β : Type u₂} [NonUnitalCommSemiring β] :
            NonUnitalCommSemiring (α →₀ β)
            Equations
              source
              instance Finsupp.instNonUnitalNonAssocRing {α : Type u₁} {β : Type u₂} [NonUnitalNonAssocRing β] :
              NonUnitalNonAssocRing (α →₀ β)
              Equations
                source
                instance Finsupp.instNonUnitalRing {α : Type u₁} {β : Type u₂} [NonUnitalRing β] :
                NonUnitalRing (α →₀ β)
                Equations
                  source
                  instance Finsupp.instNonUnitalCommRing {α : Type u₁} {β : Type u₂} [NonUnitalCommRing β] :
                  NonUnitalCommRing (α →₀ β)
                  Equations
                    source
                    instance Finsupp.pointwiseScalar {α : Type u₁} {β : Type u₂} [Semiring β] :
                    SMul (α → β) (α →₀ β)
                    Equations
                      source
                      @[simp]
                      theorem Finsupp.coe_pointwise_smul {α : Type u₁} {β : Type u₂} [Semiring β] (f : α → β) (g : α →₀ β) :
                      ⇑(f • g) = f • ⇑g
                      source
                      instance Finsupp.pointwiseModule {α : Type u₁} {β : Type u₂} [Semiring β] :
                      Module (α → β) (α →₀ β)

                      The pointwise multiplicative action of functions on finitely supported functions

                      Equations