The pointwise product on finsupp.
TODO per issue #1864:
We intend to remove the convolution product on finsupp, and define
it only on a type synonym add_monoid_algebra. After we've done this,
it would be good to make this the default product on finsupp.
Declarations about the pointwise product on finsupps
@[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.mul_apply
{α : Type u₁}
{β : Type u₂}
[mul_zero_class β]
{g₁ g₂ : α →₀ β}
{a : α} :
@[instance]
Equations
- finsupp.semigroup = {mul := has_mul.mul finsupp.has_mul, mul_assoc := _}
@[instance]
Equations
- finsupp.distrib = {mul := semigroup.mul infer_instance, add := add_comm_group.add infer_instance, left_distrib := _, right_distrib := _}