Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
```/-
Authors: Scott Morrison

! This file was ported from Lean 3 source module data.finsupp.pointwise
! leanprover-community/mathlib commit f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Finsupp.Defs
import Mathlib.Algebra.Ring.Pi

/-!
# The pointwise product on `Finsupp`.

For the convolution product on `Finsupp` when the domain has a binary operation,
(which is in turn used to define `Polynomial` and `MvPolynomial`)
and `MonoidAlgebra`.
-/

noncomputable section

open Finset

universe u₁ u₂ u₃ u₄ u₅

variable {α: Type u₁α : Type u₁: Type (u₁+1)Type u₁} {β: Type u₂β : Type u₂: Type (u₂+1)Type u₂} {γ: Type u₃γ : Type u₃: Type (u₃+1)Type u₃} {δ: Type u₄δ : Type u₄: Type (u₄+1)Type u₄} {ι: Type u₅ι : Type u₅: Type (u₅+1)Type u₅}

namespace Finsupp

/-! ### Declarations about the pointwise product on `Finsupp`s -/

section

variable [MulZeroClass: Type ?u.3444 → Type ?u.3444MulZeroClass β: Type u₂β]

/-- The product of `f g : α →₀ β` is the finitely supported function
whose value at `a` is `f a * g a`. -/
instance: {α : Type u₁} → {β : Type u₂} → [inst : MulZeroClass β] → Mul (α →₀ β)instance : Mul: Type ?u.38 → Type ?u.38Mul (α: Type u₁α →₀ β: Type u₂β) :=
⟨zipWith: {α : Type ?u.401} →
{M : Type ?u.400} →
{N : Type ?u.399} →
{P : Type ?u.398} →
[inst : Zero M] →
[inst_1 : Zero N] → [inst_2 : Zero P] → (f : M → N → P) → f 0 0 = 0 → (α →₀ M) → (α →₀ N) → α →₀ PzipWith (· * ·): β → β → β(· * ·) (mul_zero: ∀ {M₀ : Type ?u.1016} [self : MulZeroClass M₀] (a : M₀), a * 0 = 0mul_zero 0: ?m.10200)⟩

theorem coe_mul: ∀ (g₁ g₂ : α →₀ β), ↑(g₁ * g₂) = ↑g₁ * ↑g₂coe_mul (g₁: α →₀ βg₁ g₂: α →₀ βg₂ : α: Type u₁α →₀ β: Type u₂β) : ⇑(g₁: α →₀ βg₁ * g₂: α →₀ βg₂) = g₁: α →₀ βg₁ * g₂: α →₀ βg₂ :=
rfl: ∀ {α : Sort ?u.3412} {a : α}, a = arfl
#align finsupp.coe_mul Finsupp.coe_mul: ∀ {α : Type u₁} {β : Type u₂} [inst : MulZeroClass β] (g₁ g₂ : α →₀ β), ↑(g₁ * g₂) = ↑g₁ * ↑g₂Finsupp.coe_mul

@[simp]
theorem mul_apply: ∀ {g₁ g₂ : α →₀ β} {a : α}, ↑(g₁ * g₂) a = ↑g₁ a * ↑g₂ amul_apply {g₁: α →₀ βg₁ g₂: α →₀ βg₂ : α: Type u₁α →₀ β: Type u₂β} {a: αa : α: Type u₁α} : (g₁: α →₀ βg₁ * g₂: α →₀ βg₂) a: αa = g₁: α →₀ βg₁ a: αa * g₂: α →₀ βg₂ a: αa :=
rfl: ∀ {α : Sort ?u.4439} {a : α}, a = arfl
#align finsupp.mul_apply Finsupp.mul_apply: ∀ {α : Type u₁} {β : Type u₂} [inst : MulZeroClass β] {g₁ g₂ : α →₀ β} {a : α}, ↑(g₁ * g₂) a = ↑g₁ a * ↑g₂ aFinsupp.mul_apply

theorem support_mul: ∀ [inst : DecidableEq α] {g₁ g₂ : α →₀ β}, (g₁ * g₂).support ⊆ g₁.support ∩ g₂.supportsupport_mul [DecidableEq: Sort ?u.4500 → Sort (max1?u.4500)DecidableEq α: Type u₁α] {g₁: α →₀ βg₁ g₂: α →₀ βg₂ : α: Type u₁α →₀ β: Type u₂β} :
(g₁: α →₀ βg₁ * g₂: α →₀ βg₂).support: {α : Type ?u.4946} → {M : Type ?u.4945} → [inst : Zero M] → (α →₀ M) → Finset αsupport ⊆ g₁: α →₀ βg₁.support: {α : Type ?u.4965} → {M : Type ?u.4964} → [inst : Zero M] → (α →₀ M) → Finset αsupport ∩ g₂: α →₀ βg₂.support: {α : Type ?u.4970} → {M : Type ?u.4969} → [inst : Zero M] → (α →₀ M) → Finset αsupport := byGoals accomplished! 🐙
α: Type u₁β: Type u₂γ: Type u₃δ: Type u₄ι: Type u₅inst✝¹: MulZeroClass βinst✝: DecidableEq αg₁, g₂: α →₀ β(g₁ * g₂).support ⊆ g₁.support ∩ g₂.supportintro a: αa h: a ∈ (g₁ * g₂).supporthα: Type u₁β: Type u₂γ: Type u₃δ: Type u₄ι: Type u₅inst✝¹: MulZeroClass βinst✝: DecidableEq αg₁, g₂: α →₀ βa: αh: a ∈ (g₁ * g₂).supporta ∈ g₁.support ∩ g₂.support
α: Type u₁β: Type u₂γ: Type u₃δ: Type u₄ι: Type u₅inst✝¹: MulZeroClass βinst✝: DecidableEq αg₁, g₂: α →₀ β(g₁ * g₂).support ⊆ g₁.support ∩ g₂.supportsimp only [mul_apply: ∀ {α : Type ?u.5045} {β : Type ?u.5044} [inst : MulZeroClass β] {g₁ g₂ : α →₀ β} {a : α}, ↑(g₁ * g₂) a = ↑g₁ a * ↑g₂ amul_apply, mem_support_iff: ∀ {α : Type ?u.5076} {M : Type ?u.5077} [inst : Zero M] {f : α →₀ M} {a : α}, a ∈ f.support ↔ ↑f a ≠ 0mem_support_iff] at h: a ∈ (g₁ * g₂).supporthα: Type u₁β: Type u₂γ: Type u₃δ: Type u₄ι: Type u₅inst✝¹: MulZeroClass βinst✝: DecidableEq αg₁, g₂: α →₀ βa: αh: ↑g₁ a * ↑g₂ a ≠ 0a ∈ g₁.support ∩ g₂.support
α: Type u₁β: Type u₂γ: Type u₃δ: Type u₄ι: Type u₅inst✝¹: MulZeroClass βinst✝: DecidableEq αg₁, g₂: α →₀ β(g₁ * g₂).support ⊆ g₁.support ∩ g₂.supportsimp only [mem_support_iff: ∀ {α : Type ?u.5679} {M : Type ?u.5680} [inst : Zero M] {f : α →₀ M} {a : α}, a ∈ f.support ↔ ↑f a ≠ 0mem_support_iff, mem_inter: ∀ {α : Type ?u.5699} [inst : DecidableEq α] {a : α} {s₁ s₂ : Finset α}, a ∈ s₁ ∩ s₂ ↔ a ∈ s₁ ∧ a ∈ s₂mem_inter, Ne.def: ∀ {α : Sort ?u.5732} (a b : α), (a ≠ b) = ¬a = bNe.def]α: Type u₁β: Type u₂γ: Type u₃δ: Type u₄ι: Type u₅inst✝¹: MulZeroClass βinst✝: DecidableEq αg₁, g₂: α →₀ βa: αh: ↑g₁ a * ↑g₂ a ≠ 0¬↑g₁ a = 0 ∧ ¬↑g₂ a = 0
α: Type u₁β: Type u₂γ: Type u₃δ: Type u₄ι: Type u₅inst✝¹: MulZeroClass βinst✝: DecidableEq αg₁, g₂: α →₀ β(g₁ * g₂).support ⊆ g₁.support ∩ g₂.supportrw [α: Type u₁β: Type u₂γ: Type u₃δ: Type u₄ι: Type u₅inst✝¹: MulZeroClass βinst✝: DecidableEq αg₁, g₂: α →₀ βa: αh: ↑g₁ a * ↑g₂ a ≠ 0¬↑g₁ a = 0 ∧ ¬↑g₂ a = 0← not_or: ∀ {p q : Prop}, ¬(p ∨ q) ↔ ¬p ∧ ¬qnot_orα: Type u₁β: Type u₂γ: Type u₃δ: Type u₄ι: Type u₅inst✝¹: MulZeroClass βinst✝: DecidableEq αg₁, g₂: α →₀ βa: αh: ↑g₁ a * ↑g₂ a ≠ 0¬(↑g₁ a = 0 ∨ ↑g₂ a = 0)]α: Type u₁β: Type u₂γ: Type u₃δ: Type u₄ι: Type u₅inst✝¹: MulZeroClass βinst✝: DecidableEq αg₁, g₂: α →₀ βa: αh: ↑g₁ a * ↑g₂ a ≠ 0¬(↑g₁ a = 0 ∨ ↑g₂ a = 0)
α: Type u₁β: Type u₂γ: Type u₃δ: Type u₄ι: Type u₅inst✝¹: MulZeroClass βinst✝: DecidableEq αg₁, g₂: α →₀ β(g₁ * g₂).support ⊆ g₁.support ∩ g₂.supportintro w: ↑g₁ a = 0 ∨ ↑g₂ a = 0wα: Type u₁β: Type u₂γ: Type u₃δ: Type u₄ι: Type u₅inst✝¹: MulZeroClass βinst✝: DecidableEq αg₁, g₂: α →₀ βa: αh: ↑g₁ a * ↑g₂ a ≠ 0w: ↑g₁ a = 0 ∨ ↑g₂ a = 0False
α: Type u₁β: Type u₂γ: Type u₃δ: Type u₄ι: Type u₅inst✝¹: MulZeroClass βinst✝: DecidableEq αg₁, g₂: α →₀ β(g₁ * g₂).support ⊆ g₁.support ∩ g₂.supportapply h: ↑g₁ a * ↑g₂ a ≠ 0hα: Type u₁β: Type u₂γ: Type u₃δ: Type u₄ι: Type u₅inst✝¹: MulZeroClass βinst✝: DecidableEq αg₁, g₂: α →₀ βa: αh: ↑g₁ a * ↑g₂ a ≠ 0w: ↑g₁ a = 0 ∨ ↑g₂ a = 0↑g₁ a * ↑g₂ a = 0
α: Type u₁β: Type u₂γ: Type u₃δ: Type u₄ι: Type u₅inst✝¹: MulZeroClass βinst✝: DecidableEq αg₁, g₂: α →₀ β(g₁ * g₂).support ⊆ g₁.support ∩ g₂.supportcases' w: ↑g₁ a = 0 ∨ ↑g₂ a = 0w with w: ?m.6419w w: ?m.6420wα: Type u₁β: Type u₂γ: Type u₃δ: Type u₄ι: Type u₅inst✝¹: MulZeroClass βinst✝: DecidableEq αg₁, g₂: α →₀ βa: αh: ↑g₁ a * ↑g₂ a ≠ 0w: ↑g₁ a = 0inl↑g₁ a * ↑g₂ a = 0α: Type u₁β: Type u₂γ: Type u₃δ: Type u₄ι: Type u₅inst✝¹: MulZeroClass βinst✝: DecidableEq αg₁, g₂: α →₀ βa: αh: ↑g₁ a * ↑g₂ a ≠ 0w: ↑g₂ a = 0inr↑g₁ a * ↑g₂ a = 0 α: Type u₁β: Type u₂γ: Type u₃δ: Type u₄ι: Type u₅inst✝¹: MulZeroClass βinst✝: DecidableEq αg₁, g₂: α →₀ βa: αh: ↑g₁ a * ↑g₂ a ≠ 0w: ↑g₁ a = 0 ∨ ↑g₂ a = 0↑g₁ a * ↑g₂ a = 0<;>α: Type u₁β: Type u₂γ: Type u₃δ: Type u₄ι: Type u₅inst✝¹: MulZeroClass βinst✝: DecidableEq αg₁, g₂: α →₀ βa: αh: ↑g₁ a * ↑g₂ a ≠ 0w: ↑g₁ a = 0inl↑g₁ a * ↑g₂ a = 0α: Type u₁β: Type u₂γ: Type u₃δ: Type u₄ι: Type u₅inst✝¹: MulZeroClass βinst✝: DecidableEq αg₁, g₂: α →₀ βa: αh: ↑g₁ a * ↑g₂ a ≠ 0w: ↑g₂ a = 0inr↑g₁ a * ↑g₂ a = 0 α: Type u₁β: Type u₂γ: Type u₃δ: Type u₄ι: Type u₅inst✝¹: MulZeroClass βinst✝: DecidableEq αg₁, g₂: α →₀ βa: αh: ↑g₁ a * ↑g₂ a ≠ 0w: ↑g₁ a = 0 ∨ ↑g₂ a = 0↑g₁ a * ↑g₂ a = 0(α: Type u₁β: Type u₂γ: Type u₃δ: Type u₄ι: Type u₅inst✝¹: MulZeroClass βinst✝: DecidableEq αg₁, g₂: α →₀ βa: αh: ↑g₁ a * ↑g₂ a ≠ 0w: ↑g₂ a = 0inr↑g₁ a * ↑g₂ a = 0rw [α: Type u₁β: Type u₂γ: Type u₃δ: Type u₄ι: Type u₅inst✝¹: MulZeroClass βinst✝: DecidableEq αg₁, g₂: α →₀ βa: αh: ↑g₁ a * ↑g₂ a ≠ 0w: ↑g₂ a = 0inr↑g₁ a * ↑g₂ a = 0w: ?m.6420wα: Type u₁β: Type u₂γ: Type u₃δ: Type u₄ι: Type u₅inst✝¹: MulZeroClass βinst✝: DecidableEq αg₁, g₂: α →₀ βa: αh: ↑g₁ a * ↑g₂ a ≠ 0w: ↑g₂ a = 0inr↑g₁ a * 0 = 0]α: Type u₁β: Type u₂γ: Type u₃δ: Type u₄ι: Type u₅inst✝¹: MulZeroClass βinst✝: DecidableEq αg₁, g₂: α →₀ βa: αh: ↑g₁ a * ↑g₂ a ≠ 0w: ↑g₂ a = 0inr↑g₁ a * 0 = 0 α: Type u₁β: Type u₂γ: Type u₃δ: Type u₄ι: Type u₅inst✝¹: MulZeroClass βinst✝: DecidableEq αg₁, g₂: α →₀ βa: αh: ↑g₁ a * ↑g₂ a ≠ 0w: ↑g₂ a = 0inr↑g₁ a * ↑g₂ a = 0;α: Type u₁β: Type u₂γ: Type u₃δ: Type u₄ι: Type u₅inst✝¹: MulZeroClass βinst✝: DecidableEq αg₁, g₂: α →₀ βa: αh: ↑g₁ a * ↑g₂ a ≠ 0w: ↑g₁ a = 0inl0 * ↑g₂ a = 0 α: Type u₁β: Type u₂γ: Type u₃δ: Type u₄ι: Type u₅inst✝¹: MulZeroClass βinst✝: DecidableEq αg₁, g₂: α →₀ βa: αh: ↑g₁ a * ↑g₂ a ≠ 0w: ↑g₂ a = 0inr↑g₁ a * ↑g₂ a = 0simpGoals accomplished! 🐙)Goals accomplished! 🐙
#align finsupp.support_mul Finsupp.support_mul: ∀ {α : Type u₁} {β : Type u₂} [inst : MulZeroClass β] [inst_1 : DecidableEq α] {g₁ g₂ : α →₀ β},
(g₁ * g₂).support ⊆ g₁.support ∩ g₂.supportFinsupp.support_mul

instance: {α : Type u₁} → {β : Type u₂} → [inst : MulZeroClass β] → MulZeroClass (α →₀ β)instance : MulZeroClass: Type ?u.6625 → Type ?u.6625MulZeroClass (α: Type u₁α →₀ β: Type u₂β) :=
FunLike.coe_injective: ∀ {F : Sort ?u.6980} {α : Sort ?u.6981} {β : α → Sort ?u.6982} [i : FunLike F α β], Function.Injective fun f => ↑fFunLike.coe_injective.mulZeroClass: {M₀ : Type ?u.7043} →
{M₀' : Type ?u.7042} →
[inst : MulZeroClass M₀] →
[inst_1 : Mul M₀'] →
[inst_2 : Zero M₀'] →
(f : M₀' → M₀) → Function.Injective f → f 0 = 0 → (∀ (a b : M₀'), f (a * b) = f a * f b) → MulZeroClass M₀'mulZeroClass _: ?m.7054 → ?m.7053_ coe_zero: ∀ {α : Type ?u.7164} {M : Type ?u.7165} [inst : Zero M], ↑0 = 0coe_zero coe_mul: ∀ {α : Type ?u.7286} {β : Type ?u.7285} [inst : MulZeroClass β] (g₁ g₂ : α →₀ β), ↑(g₁ * g₂) = ↑g₁ * ↑g₂coe_mul

end

instance: {α : Type u₁} → {β : Type u₂} → [inst : SemigroupWithZero β] → SemigroupWithZero (α →₀ β)instance [SemigroupWithZero: Type ?u.7575 → Type ?u.7575SemigroupWithZero β: Type u₂β] : SemigroupWithZero: Type ?u.7578 → Type ?u.7578SemigroupWithZero (α: Type u₁α →₀ β: Type u₂β) :=
FunLike.coe_injective: ∀ {F : Sort ?u.7891} {α : Sort ?u.7892} {β : α → Sort ?u.7893} [i : FunLike F α β], Function.Injective fun f => ↑fFunLike.coe_injective.semigroupWithZero: {M₀ : Type ?u.7954} →
{M₀' : Type ?u.7953} →
[inst : Zero M₀'] →
[inst_1 : Mul M₀'] →
[inst_2 : SemigroupWithZero M₀] →
(f : M₀' → M₀) →
Function.Injective f → f 0 = 0 → (∀ (x y : M₀'), f (x * y) = f x * f y) → SemigroupWithZero M₀'semigroupWithZero _: ?m.7965 → ?m.7964_ coe_zero: ∀ {α : Type ?u.8073} {M : Type ?u.8074} [inst : Zero M], ↑0 = 0coe_zero coe_mul: ∀ {α : Type ?u.8429} {β : Type ?u.8428} [inst : MulZeroClass β] (g₁ g₂ : α →₀ β), ↑(g₁ * g₂) = ↑g₁ * ↑g₂coe_mul

instance: {α : Type u₁} → {β : Type u₂} → [inst : NonUnitalNonAssocSemiring β] → NonUnitalNonAssocSemiring (α →₀ β)instance [NonUnitalNonAssocSemiring: Type ?u.8991 → Type ?u.8991NonUnitalNonAssocSemiring β: Type u₂β] : NonUnitalNonAssocSemiring: Type ?u.8994 → Type ?u.8994NonUnitalNonAssocSemiring (α: Type u₁α →₀ β: Type u₂β) :=
FunLike.coe_injective: ∀ {F : Sort ?u.9357} {α : Sort ?u.9358} {β : α → Sort ?u.9359} [i : FunLike F α β], Function.Injective fun f => ↑fFunLike.coe_injective.nonUnitalNonAssocSemiring: {β : Type ?u.9419} →
[inst : Zero β] →
[inst_2 : Mul β] →
[inst_3 : SMul ℕ β] →
{α : Type ?u.9420} →
[inst_4 : NonUnitalNonAssocSemiring α] →
(f : β → α) →
Function.Injective f →
f 0 = 0 →
(∀ (x y : β), f (x + y) = f x + f y) →
(∀ (x y : β), f (x * y) = f x * f y) →
(∀ (x : β) (n : ℕ), f (n • x) = n • f x) → NonUnitalNonAssocSemiring βnonUnitalNonAssocSemiring _: ?m.9434 → ?m.9439_ coe_zero: ∀ {α : Type ?u.9597} {M : Type ?u.9598} [inst : Zero M], ↑0 = 0coe_zero coe_add: ∀ {α : Type ?u.9993} {M : Type ?u.9994} [inst : AddZeroClass M] (f g : α →₀ M), ↑(f + g) = ↑f + ↑gcoe_add coe_mul: ∀ {α : Type ?u.10459} {β : Type ?u.10458} [inst : MulZeroClass β] (g₁ g₂ : α →₀ β), ↑(g₁ * g₂) = ↑g₁ * ↑g₂coe_mul fun _: ?m.10518_ _: ?m.10521_ ↦ rfl: ∀ {α : Sort ?u.10523} {a : α}, a = arfl

instance: {α : Type u₁} → {β : Type u₂} → [inst : NonUnitalSemiring β] → NonUnitalSemiring (α →₀ β)instance [NonUnitalSemiring: Type ?u.11139 → Type ?u.11139NonUnitalSemiring β: Type u₂β] : NonUnitalSemiring: Type ?u.11142 → Type ?u.11142NonUnitalSemiring (α: Type u₁α →₀ β: Type u₂β) :=
FunLike.coe_injective: ∀ {F : Sort ?u.11462} {α : Sort ?u.11463} {β : α → Sort ?u.11464} [i : FunLike F α β], Function.Injective fun f => ↑fFunLike.coe_injective.nonUnitalSemiring: {β : Type ?u.11524} →
[inst : Zero β] →
[inst_2 : Mul β] →
[inst_3 : SMul ℕ β] →
{α : Type ?u.11525} →
[inst_4 : NonUnitalSemiring α] →
(f : β → α) →
Function.Injective f →
f 0 = 0 →
(∀ (x y : β), f (x + y) = f x + f y) →
(∀ (x y : β), f (x * y) = f x * f y) →
(∀ (x : β) (n : ℕ), f (n • x) = n • f x) → NonUnitalSemiring βnonUnitalSemiring _: ?m.11539 → ?m.11544_ coe_zero: ∀ {α : Type ?u.11702} {M : Type ?u.11703} [inst : Zero M], ↑0 = 0coe_zero coe_add: ∀ {α : Type ?u.12065} {M : Type ?u.12066} [inst : AddZeroClass M] (f g : α →₀ M), ↑(f + g) = ↑f + ↑gcoe_add coe_mul: ∀ {α : Type ?u.12546} {β : Type ?u.12545} [inst : MulZeroClass β] (g₁ g₂ : α →₀ β), ↑(g₁ * g₂) = ↑g₁ * ↑g₂coe_mul fun _: ?m.12783_ _: ?m.12786_ ↦ rfl: ∀ {α : Sort ?u.12788} {a : α}, a = arfl

instance: {α : Type u₁} → {β : Type u₂} → [inst : NonUnitalCommSemiring β] → NonUnitalCommSemiring (α →₀ β)instance [NonUnitalCommSemiring: Type ?u.13409 → Type ?u.13409NonUnitalCommSemiring β: Type u₂β] : NonUnitalCommSemiring: Type ?u.13412 → Type ?u.13412NonUnitalCommSemiring (α: Type u₁α →₀ β: Type u₂β) :=
FunLike.coe_injective: ∀ {F : Sort ?u.13738} {α : Sort ?u.13739} {β : α → Sort ?u.13740} [i : FunLike F α β], Function.Injective fun f => ↑fFunLike.coe_injective.nonUnitalCommSemiring: {α : Type ?u.13801} →
{γ : Type ?u.13800} →
[inst : NonUnitalCommSemiring α] →
[inst_1 : Zero γ] →
[inst_3 : Mul γ] →
[inst_4 : SMul ℕ γ] →
(f : γ → α) →
Function.Injective f →
f 0 = 0 →
(∀ (x y : γ), f (x + y) = f x + f y) →
(∀ (x y : γ), f (x * y) = f x * f y) →
(∀ (x : γ) (n : ℕ), f (n • x) = n • f x) → NonUnitalCommSemiring γnonUnitalCommSemiring _: ?m.13816 → ?m.13815_ coe_zero: ∀ {α : Type ?u.13976} {M : Type ?u.13977} [inst : Zero M], ↑0 = 0coe_zero coe_add: ∀ {α : Type ?u.14341} {M : Type ?u.14342} [inst : AddZeroClass M] (f g : α →₀ M), ↑(f + g) = ↑f + ↑gcoe_add coe_mul: ∀ {α : Type ?u.14826} {β : Type ?u.14825} [inst : MulZeroClass β] (g₁ g₂ : α →₀ β), ↑(g₁ * g₂) = ↑g₁ * ↑g₂coe_mul fun _: ?m.15067_ _: ?m.15070_ ↦ rfl: ∀ {α : Sort ?u.15072} {a : α}, a = arfl

instance: {α : Type u₁} → {β : Type u₂} → [inst : NonUnitalNonAssocRing β] → NonUnitalNonAssocRing (α →₀ β)instance [NonUnitalNonAssocRing: Type ?u.15699 → Type ?u.15699NonUnitalNonAssocRing β: Type u₂β] : NonUnitalNonAssocRing: Type ?u.15702 → Type ?u.15702NonUnitalNonAssocRing (α: Type u₁α →₀ β: Type u₂β) :=
FunLike.coe_injective: ∀ {F : Sort ?u.16071} {α : Sort ?u.16072} {β : α → Sort ?u.16073} [i : FunLike F α β], Function.Injective fun f => ↑fFunLike.coe_injective.nonUnitalNonAssocRing: {α : Type ?u.16134} →
{β : Type ?u.16133} →
[inst : NonUnitalNonAssocRing α] →
[inst_1 : Zero β] →
[inst_3 : Mul β] →
[inst_4 : Neg β] →
[inst_5 : Sub β] →
[inst_6 : SMul ℕ β] →
[inst_7 : SMul ℤ β] →
(f : β → α) →
Function.Injective f →
f 0 = 0 →
(∀ (x y : β), f (x + y) = f x + f y) →
(∀ (x y : β), f (x * y) = f x * f y) →
(∀ (x : β), f (-x) = -f x) →
(∀ (x y : β), f (x - y) = f x - f y) →
(∀ (x : β) (n : ℕ), f (n • x) = n • f x) →
(∀ (x : β) (n : ℤ), f (n • x) = n • f x) → NonUnitalNonAssocRing βnonUnitalNonAssocRing _: ?m.16155 → ?m.16154_ coe_zero: ∀ {α : Type ?u.16390} {M : Type ?u.16391} [inst : Zero M], ↑0 = 0coe_zero coe_add: ∀ {α : Type ?u.16788} {M : Type ?u.16789} [inst : AddZeroClass M] (f g : α →₀ M), ↑(f + g) = ↑f + ↑gcoe_add coe_mul: ∀ {α : Type ?u.17102} {β : Type ?u.17101} [inst : MulZeroClass β] (g₁ g₂ : α →₀ β), ↑(g₁ * g₂) = ↑g₁ * ↑g₂coe_mul coe_neg: ∀ {α : Type ?u.17165} {G : Type ?u.17164} [inst : NegZeroClass G] (g : α →₀ G), ↑(-g) = -↑gcoe_neg coe_sub: ∀ {α : Type ?u.17290} {G : Type ?u.17289} [inst : SubNegZeroMonoid G] (g₁ g₂ : α →₀ G), ↑(g₁ - g₂) = ↑g₁ - ↑g₂coe_sub
(fun _: ?m.17430_ _: ?m.17433_ ↦ rfl: ∀ {α : Sort ?u.17435} {a : α}, a = arfl) fun _: ?m.17704_ _: ?m.17707_ ↦ rfl: ∀ {α : Sort ?u.17709} {a : α}, a = arfl

instance: {α : Type u₁} → {β : Type u₂} → [inst : NonUnitalRing β] → NonUnitalRing (α →₀ β)instance [NonUnitalRing: Type ?u.18052 → Type ?u.18052NonUnitalRing β: Type u₂β] : NonUnitalRing: Type ?u.18055 → Type ?u.18055NonUnitalRing (α: Type u₁α →₀ β: Type u₂β) :=
FunLike.coe_injective: ∀ {F : Sort ?u.18398} {α : Sort ?u.18399} {β : α → Sort ?u.18400} [i : FunLike F α β], Function.Injective fun f => ↑fFunLike.coe_injective.nonUnitalRing: {α : Type ?u.18461} →
{β : Type ?u.18460} →
[inst : NonUnitalRing α] →
[inst_1 : Zero β] →
[inst_3 : Mul β] →
[inst_4 : Neg β] →
[inst_5 : Sub β] →
[inst_6 : SMul ℕ β] →
[inst_7 : SMul ℤ β] →
(f : β → α) →
Function.Injective f →
f 0 = 0 →
(∀ (x y : β), f (x + y) = f x + f y) →
(∀ (x y : β), f (x * y) = f x * f y) →
(∀ (x : β), f (-x) = -f x) →
(∀ (x y : β), f (x - y) = f x - f y) →
(∀ (x : β) (n : ℕ), f (n • x) = n • f x) →
(∀ (x : β) (n : ℤ), f (n • x) = n • f x) → NonUnitalRing βnonUnitalRing _: ?m.18482 → ?m.18481_ coe_zero: ∀ {α : Type ?u.18717} {M : Type ?u.18718} [inst : Zero M], ↑0 = 0coe_zero coe_add: ∀ {α : Type ?u.19095} {M : Type ?u.19096} [inst : AddZeroClass M] (f g : α →₀ M), ↑(f + g) = ↑f + ↑gcoe_add coe_mul: ∀ {α : Type ?u.19417} {β : Type ?u.19416} [inst : MulZeroClass β] (g₁ g₂ : α →₀ β), ↑(g₁ * g₂) = ↑g₁ * ↑g₂coe_mul coe_neg: ∀ {α : Type ?u.19543} {G : Type ?u.19542} [inst : NegZeroClass G] (g : α →₀ G), ↑(-g) = -↑gcoe_neg coe_sub: ∀ {α : Type ?u.19677} {G : Type ?u.19676} [inst : SubNegZeroMonoid G] (g₁ g₂ : α →₀ G), ↑(g₁ - g₂) = ↑g₁ - ↑g₂coe_sub (fun _: ?m.19826_ _: ?m.19829_ ↦ rfl: ∀ {α : Sort ?u.19831} {a : α}, a = arfl)
fun _: ?m.20107_ _: ?m.20110_ ↦ rfl: ∀ {α : Sort ?u.20112} {a : α}, a = arfl

instance: {α : Type u₁} → {β : Type u₂} → [inst : NonUnitalCommRing β] → NonUnitalCommRing (α →₀ β)instance [NonUnitalCommRing: Type ?u.20427 → Type ?u.20427NonUnitalCommRing β: Type u₂β] : NonUnitalCommRing: Type ?u.20430 → Type ?u.20430NonUnitalCommRing (α: Type u₁α →₀ β: Type u₂β) :=
FunLike.coe_injective: ∀ {F : Sort ?u.20761} {α : Sort ?u.20762} {β : α → Sort ?u.20763} [i : FunLike F α β], Function.Injective fun f => ↑fFunLike.coe_injective.nonUnitalCommRing: {α : Type ?u.20824} →
{β : Type ?u.20823} →
[inst : NonUnitalCommRing α] →
[inst_1 : Zero β] →
[inst_3 : Mul β] →
[inst_4 : Neg β] →
[inst_5 : Sub β] →
[inst_6 : SMul ℕ β] →
[inst_7 : SMul ℤ β] →
(f : β → α) →
Function.Injective f →
f 0 = 0 →
(∀ (x y : β), f (x + y) = f x + f y) →
(∀ (x y : β), f (x * y) = f x * f y) →
(∀ (x : β), f (-x) = -f x) →
(∀ (x y : β), f (x - y) = f x - f y) →
(∀ (x : β) (n : ℕ), f (n • x) = n • f x) →
(∀ (x : β) (n : ℤ), f (n • x) = n • f x) → NonUnitalCommRing βnonUnitalCommRing _: ?m.20845 → ?m.20844_ coe_zero: ∀ {α : Type ?u.21078} {M : Type ?u.21079} [inst : Zero M], ↑0 = 0coe_zero coe_add: ∀ {α : Type ?u.21444} {M : Type ?u.21445} [inst : AddZeroClass M] (f g : α →₀ M), ↑(f + g) = ↑f + ↑gcoe_add coe_mul: ∀ {α : Type ?u.21771} {β : Type ?u.21770} [inst : MulZeroClass β] (g₁ g₂ : α →₀ β), ↑(g₁ * g₂) = ↑g₁ * ↑g₂coe_mul coe_neg: ∀ {α : Type ?u.21900} {G : Type ?u.21899} [inst : NegZeroClass G] (g : α →₀ G), ↑(-g) = -↑gcoe_neg coe_sub: ∀ {α : Type ?u.22037} {G : Type ?u.22036} [inst : SubNegZeroMonoid G] (g₁ g₂ : α →₀ G), ↑(g₁ - g₂) = ↑g₁ - ↑g₂coe_sub
(fun _: ?m.22189_ _: ?m.22192_ ↦ rfl: ∀ {α : Sort ?u.22194} {a : α}, a = arfl) fun _: ?m.22474_ _: ?m.22477_ ↦ rfl: ∀ {α : Sort ?u.22479} {a : α}, a = arfl

-- TODO can this be generalized in the direction of `Pi.smul'`
-- (i.e. dependent functions and finsupps)
-- TODO in theory this could be generalised, we only really need `smul_zero` for the definition
instance pointwiseScalar: [inst : Semiring β] → SMul (α → β) (α →₀ β)pointwiseScalar [Semiring: Type ?u.22796 → Type ?u.22796Semiring β: Type u₂β] : SMul: Type ?u.22800 → Type ?u.22799 → Type (max?u.22800?u.22799)SMul (α: Type u₁α → β: Type u₂β) (α: Type u₁α →₀ β: Type u₂β) where
smul f: ?m.22979f g: ?m.22982g :=
Finsupp.ofSupportFinite: {α : Type ?u.22985} → {M : Type ?u.22984} → [inst : Zero M] → (f : α → M) → Set.Finite (Function.support f) → α →₀ MFinsupp.ofSupportFinite (fun a: ?m.23033a ↦ f: ?m.22979f a: ?m.23033a • g: ?m.22982g a: ?m.23033a) (byGoals accomplished! 🐙
α: Type u₁β: Type u₂γ: Type u₃δ: Type u₄ι: Type u₅inst✝: Semiring βf: α → βg: α →₀ βSet.Finite (Function.support fun a => f a • ↑g a)apply Set.Finite.subset: ∀ {α : Type ?u.23640} {s : Set α}, Set.Finite s → ∀ {t : Set α}, t ⊆ s → Set.Finite tSet.Finite.subset g: α →₀ βg.finite_support: ∀ {α : Type ?u.23643} {M : Type ?u.23644} [inst : Zero M] (f : α →₀ M), Set.Finite (Function.support ↑f)finite_supportα: Type u₁β: Type u₂γ: Type u₃δ: Type u₄ι: Type u₅inst✝: Semiring βf: α → βg: α →₀ β(Function.support fun a => f a • ↑g a) ⊆ Function.support ↑g
α: Type u₁β: Type u₂γ: Type u₃δ: Type u₄ι: Type u₅inst✝: Semiring βf: α → βg: α →₀ βSet.Finite (Function.support fun a => f a • ↑g a)simp only [Function.support_subset_iff: ∀ {α : Type ?u.23674} {M : Type ?u.23675} [inst : Zero M] {f : α → M} {s : Set α},
Function.support f ⊆ s ↔ ∀ (x : α), f x ≠ 0 → x ∈ sFunction.support_subset_iff, Finsupp.mem_support_iff: ∀ {α : Type ?u.23706} {M : Type ?u.23707} [inst : Zero M] {f : α →₀ M} {a : α}, a ∈ f.support ↔ ↑f a ≠ 0Finsupp.mem_support_iff, Ne.def: ∀ {α : Sort ?u.23734} (a b : α), (a ≠ b) = ¬a = bNe.def,
Finsupp.fun_support_eq: ∀ {α : Type ?u.23746} {M : Type ?u.23747} [inst : Zero M] (f : α →₀ M), Function.support ↑f = ↑f.supportFinsupp.fun_support_eq, Finset.mem_coe: ∀ {α : Type ?u.23767} {a : α} {s : Finset α}, a ∈ ↑s ↔ a ∈ sFinset.mem_coe]α: Type u₁β: Type u₂γ: Type u₃δ: Type u₄ι: Type u₅inst✝: Semiring βf: α → βg: α →₀ β∀ (x : α), ¬f x • ↑g x = 0 → ¬↑g x = 0
α: Type u₁β: Type u₂γ: Type u₃δ: Type u₄ι: Type u₅inst✝: Semiring βf: α → βg: α →₀ βSet.Finite (Function.support fun a => f a • ↑g a)intro x: αx hx: ¬f x • ↑g x = 0hx h: ↑g x = 0hα: Type u₁β: Type u₂γ: Type u₃δ: Type u₄ι: Type u₅inst✝: Semiring βf: α → βg: α →₀ βx: αhx: ¬f x • ↑g x = 0h: ↑g x = 0False
α: Type u₁β: Type u₂γ: Type u₃δ: Type u₄ι: Type u₅inst✝: Semiring βf: α → βg: α →₀ βSet.Finite (Function.support fun a => f a • ↑g a)apply hx: ¬f x • ↑g x = 0hxα: Type u₁β: Type u₂γ: Type u₃δ: Type u₄ι: Type u₅inst✝: Semiring βf: α → βg: α →₀ βx: αhx: ¬f x • ↑g x = 0h: ↑g x = 0f x • ↑g x = 0
α: Type u₁β: Type u₂γ: Type u₃δ: Type u₄ι: Type u₅inst✝: Semiring βf: α → βg: α →₀ βSet.Finite (Function.support fun a => f a • ↑g a)rw [α: Type u₁β: Type u₂γ: Type u₃δ: Type u₄ι: Type u₅inst✝: Semiring βf: α → βg: α →₀ βx: αhx: ¬f x • ↑g x = 0h: ↑g x = 0f x • ↑g x = 0h: ↑g x = 0h,α: Type u₁β: Type u₂γ: Type u₃δ: Type u₄ι: Type u₅inst✝: Semiring βf: α → βg: α →₀ βx: αhx: ¬f x • ↑g x = 0h: ↑g x = 0f x • 0 = 0 α: Type u₁β: Type u₂γ: Type u₃δ: Type u₄ι: Type u₅inst✝: Semiring βf: α → βg: α →₀ βx: αhx: ¬f x • ↑g x = 0h: ↑g x = 0f x • ↑g x = 0smul_zero: ∀ {M : Type ?u.24379} {A : Type ?u.24378} [inst : Zero A] [inst_1 : SMulZeroClass M A] (a : M), a • 0 = 0smul_zeroα: Type u₁β: Type u₂γ: Type u₃δ: Type u₄ι: Type u₅inst✝: Semiring βf: α → βg: α →₀ βx: αhx: ¬f x • ↑g x = 0h: ↑g x = 00 = 0]Goals accomplished! 🐙)
#align finsupp.pointwise_scalar Finsupp.pointwiseScalar: {α : Type u₁} → {β : Type u₂} → [inst : Semiring β] → SMul (α → β) (α →₀ β)Finsupp.pointwiseScalar

@[simp]
theorem coe_pointwise_smul: ∀ {α : Type u₁} {β : Type u₂} [inst : Semiring β] (f : α → β) (g : α →₀ β), ↑(f • g) = ↑(f • g)coe_pointwise_smul [Semiring: Type ?u.25101 → Type ?u.25101Semiring β: Type u₂β] (f: α → βf : α: Type u₁α → β: Type u₂β) (g: α →₀ βg : α: Type u₁α →₀ β: Type u₂β) : FunLike.coe: {F : Sort ?u.25278} →
{α : outParam (Sort ?u.25277)} → {β : outParam (α → Sort ?u.25276)} → [self : FunLike F α β] → F → (a : α) → β aFunLike.coe (f: α → βf • g: α →₀ βg) = f: α → βf • g: α →₀ βg :=
rfl: ∀ {α : Sort ?u.25621} {a : α}, a = arfl
#align finsupp.coe_pointwise_smul Finsupp.coe_pointwise_smul: ∀ {α : Type u₁} {β : Type u₂} [inst : Semiring β] (f : α → β) (g : α →₀ β), ↑(f • g) = ↑(f • g)Finsupp.coe_pointwise_smul

/-- The pointwise multiplicative action of functions on finitely supported functions -/
instance pointwiseModule: {α : Type u₁} → {β : Type u₂} → [inst : Semiring β] → Module (α → β) (α →₀ β)pointwiseModule [Semiring: Type ?u.25673 → Type ?u.25673Semiring β: Type u₂β] : Module: (R : Type ?u.25677) →
(M : Type ?u.25676) → [inst : Semiring R] → [inst : AddCommMonoid M] → Type (max?u.25677?u.25676)Module (α: Type u₁α → β: Type u₂β) (α: Type u₁α →₀ β: Type u₂β) :=
Function.Injective.module: (R : Type ?u.26163) →
{M : Type ?u.26162} →
{M₂ : Type ?u.26161} →
[inst : Semiring R] →