The pointwise product on finsupp. #
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.
@[protected, instance]
The product of f g : α →₀ β is the finitely supported function
whose value at a is f a * g a.
Equations
- finsupp.has_mul = {mul := finsupp.zip_with has_mul.mul finsupp.has_mul._proof_1}
@[simp]
theorem
finsupp.support_mul
{α : Type u₁}
{β : Type u₂}
[mul_zero_class β]
[decidable_eq α]
{g₁ g₂ : α →₀ β} :
@[protected, instance]
noncomputable
def
finsupp.mul_zero_class
{α : Type u₁}
{β : Type u₂}
[mul_zero_class β] :
mul_zero_class (α →₀ β)
Equations
- finsupp.mul_zero_class = {mul := has_mul.mul finsupp.has_mul, zero := 0, zero_mul := _, mul_zero := _}
@[protected, instance]
noncomputable
def
finsupp.semigroup_with_zero
{α : Type u₁}
{β : Type u₂}
[semigroup_with_zero β] :
semigroup_with_zero (α →₀ β)
Equations
- finsupp.semigroup_with_zero = {mul := has_mul.mul finsupp.has_mul, mul_assoc := _, zero := mul_zero_class.zero infer_instance, zero_mul := _, mul_zero := _}
@[protected, instance]
noncomputable
def
finsupp.non_unital_non_assoc_semiring
{α : Type u₁}
{β : Type u₂}
[non_unital_non_assoc_semiring β] :
Equations
- finsupp.non_unital_non_assoc_semiring = {add := add_comm_monoid.add infer_instance, add_assoc := _, zero := mul_zero_class.zero infer_instance, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul infer_instance, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := mul_zero_class.mul infer_instance, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _}
@[protected, instance]
noncomputable
def
finsupp.non_unital_semiring
{α : Type u₁}
{β : Type u₂}
[non_unital_semiring β] :
non_unital_semiring (α →₀ β)
Equations
- finsupp.non_unital_semiring = {add := non_unital_non_assoc_semiring.add infer_instance, add_assoc := _, zero := non_unital_non_assoc_semiring.zero infer_instance, zero_add := _, add_zero := _, nsmul := non_unital_non_assoc_semiring.nsmul infer_instance, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := semigroup.mul infer_instance, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _}
@[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 = {add := add_comm_group.add infer_instance, add_assoc := _, zero := mul_zero_class.zero infer_instance, zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul infer_instance, nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg infer_instance, sub := add_comm_group.sub infer_instance, sub_eq_add_neg := _, zsmul := add_comm_group.zsmul infer_instance, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := mul_zero_class.mul infer_instance, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _}
@[protected, instance]
The pointwise multiplicative action of functions on finitely supported functions
Equations
- finsupp.pointwise_module = {to_distrib_mul_action := {to_mul_action := {to_has_scalar := {smul := λ (f : α → β) (g : α →₀ β), finsupp.of_support_finite (λ (a : α), f a • ⇑g a) _}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}