mathlib3 documentation

data.finsupp.pointwise

The pointwise product on finsupp. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

For the convolution product on finsupp when the domain has a binary operation, see the type synonyms add_monoid_algebra (which is in turn used to define polynomial and mv_polynomial) and monoid_algebra.

Declarations about the pointwise product on finsupps #

source
@[protected, instance]
noncomputable def finsupp.has_mul {α : Type u₁} {β : Type u₂} [mul_zero_class β] :
has_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₂} [mul_zero_class β] (g₁ g₂ : α →₀ β) :
⇑(g₁ * g₂) = ⇑g₁ * ⇑g₂
source
@[simp]
theorem finsupp.mul_apply {α : Type u₁} {β : Type u₂} [mul_zero_class β] {g₁ g₂ : α →₀ β} {a : α} :
⇑(g₁ * g₂) a = ⇑g₁ a * ⇑g₂ a
source
theorem finsupp.support_mul {α : Type u₁} {β : Type u₂} [mul_zero_class β] [decidable_eq α] {g₁ g₂ : α →₀ β} :
(g₁ * g₂).support ⊆ g₁.support ∩ g₂.support
source
@[protected, instance]
noncomputable def finsupp.mul_zero_class {α : Type u₁} {β : Type u₂} [mul_zero_class β] :
mul_zero_class (α →₀ β)
Equations
source
@[protected, instance]
noncomputable def finsupp.semigroup_with_zero {α : Type u₁} {β : Type u₂} [semigroup_with_zero β] :
semigroup_with_zero (α →₀ β)
Equations
source
@[protected, instance]
noncomputable def finsupp.non_unital_non_assoc_semiring {α : Type u₁} {β : Type u₂} [non_unital_non_assoc_semiring β] :
non_unital_non_assoc_semiring (α →₀ β)
Equations
source
@[protected, instance]
noncomputable def finsupp.non_unital_semiring {α : Type u₁} {β : Type u₂} [non_unital_semiring β] :
non_unital_semiring (α →₀ β)
Equations
source
@[protected, instance]
noncomputable def finsupp.non_unital_comm_semiring {α : Type u₁} {β : Type u₂} [non_unital_comm_semiring β] :
non_unital_comm_semiring (α →₀ β)
Equations
source
@[protected, instance]
noncomputable def finsupp.non_unital_non_assoc_ring {α : Type u₁} {β : Type u₂} [non_unital_non_assoc_ring β] :
non_unital_non_assoc_ring (α →₀ β)
Equations
  • finsupp.non_unital_non_assoc_ring = function.injective.non_unital_non_assoc_ring coe_fn finsupp.non_unital_non_assoc_ring._proof_1 finsupp.non_unital_non_assoc_ring._proof_2 finsupp.non_unital_non_assoc_ring._proof_3 finsupp.non_unital_non_assoc_ring._proof_4 finsupp.non_unital_non_assoc_ring._proof_5 finsupp.non_unital_non_assoc_ring._proof_6 finsupp.non_unital_non_assoc_ring._proof_7 finsupp.non_unital_non_assoc_ring._proof_8
source
@[protected, instance]
noncomputable def finsupp.non_unital_ring {α : Type u₁} {β : Type u₂} [non_unital_ring β] :
non_unital_ring (α →₀ β)
Equations
  • finsupp.non_unital_ring = function.injective.non_unital_ring coe_fn finsupp.non_unital_ring._proof_1 finsupp.non_unital_ring._proof_2 finsupp.non_unital_ring._proof_3 finsupp.non_unital_ring._proof_4 finsupp.non_unital_ring._proof_5 finsupp.non_unital_ring._proof_6 finsupp.non_unital_ring._proof_7 finsupp.non_unital_ring._proof_8
source
@[protected, instance]
noncomputable def finsupp.non_unital_comm_ring {α : Type u₁} {β : Type u₂} [non_unital_comm_ring β] :
non_unital_comm_ring (α →₀ β)
Equations
  • finsupp.non_unital_comm_ring = function.injective.non_unital_comm_ring coe_fn finsupp.non_unital_comm_ring._proof_1 finsupp.non_unital_comm_ring._proof_2 finsupp.non_unital_comm_ring._proof_3 finsupp.non_unital_comm_ring._proof_4 finsupp.non_unital_comm_ring._proof_5 finsupp.non_unital_comm_ring._proof_6 finsupp.non_unital_comm_ring._proof_7 finsupp.non_unital_comm_ring._proof_8
source
@[protected, instance]
noncomputable def finsupp.pointwise_scalar {α : Type u₁} {β : Type u₂} [semiring β] :
has_smul (α → β) (α →₀ β)
Equations
source
@[simp]
theorem finsupp.coe_pointwise_smul {α : Type u₁} {β : Type u₂} [semiring β] (f : α → β) (g : α →₀ β) :
⇑(f • g) = f • ⇑g
source
@[protected, instance]
noncomputable def finsupp.pointwise_module {α : Type u₁} {β : Type u₂} [semiring β] :
module (α → β) (α →₀ β)

The pointwise multiplicative action of functions on finitely supported functions

Equations