Mathlib.Data.DFinsupp.Module

DFinsupp.instSMulOfDistribMulAction instance

[Monoid γ] [∀ i, AddMonoid (β i)] [∀ i, DistribMulAction γ (β i)] : SMul γ (Π₀ i, β i)

Full source

/-- Dependent functions with finite support inherit a semiring action from an action on each
coordinate. -/
instance [Monoid γ] [∀ i, AddMonoid (β i)] [∀ i, DistribMulAction γ (β i)] : SMul γ (Π₀ i, β i) :=
  ⟨fun c v => v.mapRange (fun _ => (c • ·)) fun _ => smul_zero _⟩

Scalar Multiplication on Dependent Functions with Finite Support

Informal description

For any monoid $\gamma$ and a family of additive monoids $\beta_i$ indexed by $i$, where each $\beta_i$ is equipped with a distributive multiplicative action by $\gamma$, the dependent functions with finite support $\Pi_{i} \beta_i$ inherit a scalar multiplication structure from $\gamma$.

DFinsupp.smul_apply theorem

 [Monoid γ] [∀ i, AddMonoid (β i)] [∀ i, DistribMulAction γ (β i)] (b : γ) (v : Π₀ i, β i) (i : ι) : (b • v) i = b • v i

Full source

theorem smul_apply [Monoid γ] [∀ i, AddMonoid (β i)] [∀ i, DistribMulAction γ (β i)] (b : γ)
    (v : Π₀ i, β i) (i : ι) : (b • v) i = b • v i :=
  rfl

Pointwise Scalar Multiplication on Dependent Functions with Finite Support

Informal description

Let $\gamma$ be a monoid, and let $\{\beta_i\}_{i \in \iota}$ be a family of additive monoids, each equipped with a distributive multiplicative action by $\gamma$. For any scalar $b \in \gamma$ and any dependent function $v \in \Pi_{i \in \iota} \beta_i$ with finite support, the evaluation of the scalar multiple $b \cdot v$ at any index $i \in \iota$ satisfies $(b \cdot v)(i) = b \cdot v(i)$.

DFinsupp.coe_smul theorem

 [Monoid γ] [∀ i, AddMonoid (β i)] [∀ i, DistribMulAction γ (β i)] (b : γ) (v : Π₀ i, β i) : ⇑(b • v) = b • ⇑v

Full source

@[simp, norm_cast]
theorem coe_smul [Monoid γ] [∀ i, AddMonoid (β i)] [∀ i, DistribMulAction γ (β i)] (b : γ)
    (v : Π₀ i, β i) : ⇑(b • v) = b • ⇑v :=
  rfl

Pointwise Scalar Multiplication on Dependent Functions with Finite Support

Informal description

Let $\gamma$ be a monoid and $\beta_i$ be a family of additive monoids indexed by $i \in \iota$, where each $\beta_i$ is equipped with a distributive multiplicative action by $\gamma$. For any $b \in \gamma$ and any dependent function with finite support $v \in \Pi_{i} \beta_i$, the function representation of the scalar multiple $b \cdot v$ is equal to the pointwise scalar multiple of $b$ with the function representation of $v$, i.e., $(b \cdot v)(i) = b \cdot v(i)$ for all $i \in \iota$.

DFinsupp.smulCommClass instance

 {δ : Type*} [Monoid γ] [Monoid δ] [∀ i, AddMonoid (β i)] [∀ i, DistribMulAction γ (β i)]
  [∀ i, DistribMulAction δ (β i)] [∀ i, SMulCommClass γ δ (β i)] : SMulCommClass γ δ (Π₀ i, β i)

Full source

instance smulCommClass {δ : Type*} [Monoid γ] [Monoid δ] [∀ i, AddMonoid (β i)]
    [∀ i, DistribMulAction γ (β i)] [∀ i, DistribMulAction δ (β i)] [∀ i, SMulCommClass γ δ (β i)] :
    SMulCommClass γ δ (Π₀ i, β i) where
  smul_comm r s m := ext fun i => by simp only [smul_apply, smul_comm r s (m i)]

Commuting Scalar Actions on Dependent Functions with Finite Support

Informal description

For any two monoids $\gamma$ and $\delta$, and a family of additive monoids $\beta_i$ indexed by $i$, where each $\beta_i$ is equipped with distributive multiplicative actions by both $\gamma$ and $\delta$ such that the actions commute (i.e., $g \cdot (h \cdot x) = h \cdot (g \cdot x)$ for all $g \in \gamma$, $h \in \delta$, and $x \in \beta_i$), the dependent functions with finite support $\Pi_{i} \beta_i$ inherit a commuting scalar multiplication structure from $\gamma$ and $\delta$.

DFinsupp.isScalarTower instance

 {δ : Type*} [Monoid γ] [Monoid δ] [∀ i, AddMonoid (β i)] [∀ i, DistribMulAction γ (β i)]
  [∀ i, DistribMulAction δ (β i)] [SMul γ δ] [∀ i, IsScalarTower γ δ (β i)] : IsScalarTower γ δ (Π₀ i, β i)

Full source

instance isScalarTower {δ : Type*} [Monoid γ] [Monoid δ] [∀ i, AddMonoid (β i)]
    [∀ i, DistribMulAction γ (β i)] [∀ i, DistribMulAction δ (β i)] [SMul γ δ]
    [∀ i, IsScalarTower γ δ (β i)] : IsScalarTower γ δ (Π₀ i, β i) where
  smul_assoc r s m := ext fun i => by simp only [smul_apply, smul_assoc r s (m i)]

Scalar Tower Structure on Dependent Functions with Finite Support

Informal description

For any monoids $\gamma$ and $\delta$, and a family of additive monoids $\beta_i$ indexed by $i$, where each $\beta_i$ is equipped with distributive multiplicative actions by both $\gamma$ and $\delta$, and $\gamma$ acts on $\delta$ via scalar multiplication, if for each $i$ the actions of $\gamma$ and $\delta$ on $\beta_i$ form a scalar tower (i.e., $(g \cdot d) \cdot b_i = g \cdot (d \cdot b_i)$ for all $g \in \gamma$, $d \in \delta$, $b_i \in \beta_i$), then the induced actions on the dependent functions with finite support $\Pi_{i} \beta_i$ also form a scalar tower.

DFinsupp.isCentralScalar instance

 [Monoid γ] [∀ i, AddMonoid (β i)] [∀ i, DistribMulAction γ (β i)] [∀ i, DistribMulAction γᵐᵒᵖ (β i)]
  [∀ i, IsCentralScalar γ (β i)] : IsCentralScalar γ (Π₀ i, β i)

Full source

instance isCentralScalar [Monoid γ] [∀ i, AddMonoid (β i)] [∀ i, DistribMulAction γ (β i)]
    [∀ i, DistribMulAction γᵐᵒᵖ (β i)] [∀ i, IsCentralScalar γ (β i)] :
    IsCentralScalar γ (Π₀ i, β i) where
  op_smul_eq_smul r m := ext fun i => by simp only [smul_apply, op_smul_eq_smul r (m i)]

Central Scalar Multiplication on Dependent Functions with Finite Support

Informal description

For any monoid $\gamma$ and a family of additive monoids $\beta_i$ indexed by $i$, where each $\beta_i$ is equipped with a distributive multiplicative action by $\gamma$ and its opposite monoid $\gamma^{\mathrm{op}}$, if the actions of $\gamma$ and $\gamma^{\mathrm{op}}$ on each $\beta_i$ are central (i.e., they coincide), then the induced scalar multiplication on the dependent functions with finite support $\Pi_{i} \beta_i$ is also central.

DFinsupp.distribMulAction instance

[Monoid γ] [∀ i, AddMonoid (β i)] [∀ i, DistribMulAction γ (β i)] : DistribMulAction γ (Π₀ i, β i)

Full source

/-- Dependent functions with finite support inherit a `DistribMulAction` structure from such a
structure on each coordinate. -/
instance distribMulAction [Monoid γ] [∀ i, AddMonoid (β i)] [∀ i, DistribMulAction γ (β i)] :
    DistribMulAction γ (Π₀ i, β i) :=
  Function.Injective.distribMulAction coeFnAddMonoidHom DFunLike.coe_injective coe_smul

Pointwise Distributive Multiplicative Action on Dependent Functions with Finite Support

Informal description

For any monoid $\gamma$ and a family of additive monoids $\beta_i$ indexed by $i$, where each $\beta_i$ is equipped with a distributive multiplicative action by $\gamma$, the type $\Pi₀ i, \beta_i$ of dependent functions with finite support inherits a distributive multiplicative action by $\gamma$ defined pointwise.

DFinsupp.module instance

[Semiring γ] [∀ i, AddCommMonoid (β i)] [∀ i, Module γ (β i)] : Module γ (Π₀ i, β i)

Full source

/-- Dependent functions with finite support inherit a module structure from such a structure on
each coordinate. -/
instance module [Semiring γ] [∀ i, AddCommMonoid (β i)] [∀ i, Module γ (β i)] :
    Module γ (Π₀ i, β i) :=
  { inferInstanceAs (DistribMulAction γ (Π₀ i, β i)) with
    zero_smul := fun c => ext fun i => by simp only [smul_apply, zero_smul, zero_apply]
    add_smul := fun c x y => ext fun i => by simp only [add_apply, smul_apply, add_smul] }

Module Structure on Dependent Functions with Finite Support

Informal description

For any semiring $\gamma$ and a family of additive commutative monoids $\beta_i$ indexed by $i$, where each $\beta_i$ is equipped with a $\gamma$-module structure, the type $\Pi₀ i, \beta_i$ of dependent functions with finite support forms a $\gamma$-module under pointwise scalar multiplication.

DFinsupp.coeFnLinearMap definition

[Semiring γ] [∀ i, AddCommMonoid (β i)] [∀ i, Module γ (β i)] : (Π₀ i, β i) →ₗ[γ] ∀ i, β i

Full source

/-- Coercion from a `DFinsupp` to a pi type is a `LinearMap`. -/
def coeFnLinearMap [Semiring γ] [∀ i, AddCommMonoid (β i)] [∀ i, Module γ (β i)] :
    (Π₀ i, β i) →ₗ[γ] ∀ i, β i where
  toFun := (⇑)
  map_add' := coe_add
  map_smul' := coe_smul

Linear map from dependent functions with finite support to dependent functions

Informal description

The linear map that coerces a dependent function with finite support `Π₀ i, β i` to a dependent function `∀ i, β i`, where each `β i` is an additive commutative monoid with a `γ`-module structure. This map preserves addition and scalar multiplication.

DFinsupp.coeFnLinearMap_apply theorem

[Semiring γ] [∀ i, AddCommMonoid (β i)] [∀ i, Module γ (β i)] (v : Π₀ i, β i) : coeFnLinearMap γ v = v

Full source

@[simp]
lemma coeFnLinearMap_apply [Semiring γ] [∀ i, AddCommMonoid (β i)] [∀ i, Module γ (β i)]
    (v : Π₀ i, β i) : coeFnLinearMap γ v = v :=
  rfl

Identity Property of the Linear Map from Finite Support Functions to Dependent Functions

Informal description

For any semiring $\gamma$ and a family of additive commutative monoids $\beta_i$ indexed by $i$, where each $\beta_i$ is equipped with a $\gamma$-module structure, the linear map `coeFnLinearMap` from dependent functions with finite support $\Pi₀ i, \beta_i$ to dependent functions $\forall i, \beta_i$ satisfies `coeFnLinearMap γ v = v` for any $v \in \Pi₀ i, \beta_i$.

DFinsupp.filter_smul theorem

 [Monoid γ] [∀ i, AddMonoid (β i)] [∀ i, DistribMulAction γ (β i)] (p : ι → Prop) [DecidablePred p] (r : γ)
  (f : Π₀ i, β i) : (r • f).filter p = r • f.filter p

Full source

@[simp]
theorem filter_smul [Monoid γ] [∀ i, AddMonoid (β i)] [∀ i, DistribMulAction γ (β i)] (p : ι → Prop)
    [DecidablePred p] (r : γ) (f : Π₀ i, β i) : (r • f).filter p = r • f.filter p := by
  ext
  simp [smul_apply, smul_ite]

Compatibility of Scalar Multiplication with Filtering in Dependent Functions

Informal description

Let $\gamma$ be a monoid and $\{\beta_i\}_{i \in \iota}$ be a family of additive monoids, each equipped with a distributive multiplicative action by $\gamma$. For any predicate $p : \iota \to \text{Prop}$ (decidable on $\iota$), scalar $r \in \gamma$, and dependent function $f \in \Pi_{i} \beta_i$ with finite support, the following equality holds: $$(r \cdot f)\big|_{p} = r \cdot (f\big|_{p})$$ where $\cdot$ denotes the scalar multiplication and $\big|_{p}$ denotes the filtering operation that restricts the function to indices satisfying $p$.

DFinsupp.filterLinearMap definition

 [Semiring γ] [∀ i, AddCommMonoid (β i)] [∀ i, Module γ (β i)] (p : ι → Prop) [DecidablePred p] :
  (Π₀ i, β i) →ₗ[γ] Π₀ i, β i

Full source

/-- `DFinsupp.filter` as a `LinearMap`. -/
@[simps]
def filterLinearMap [Semiring γ] [∀ i, AddCommMonoid (β i)] [∀ i, Module γ (β i)] (p : ι → Prop)
    [DecidablePred p] : (Π₀ i, β i) →ₗ[γ] Π₀ i, β i where
  toFun := filter p
  map_add' := filter_add p
  map_smul' := filter_smul p

Linear map of filtering for dependent functions with finite support

Informal description

For a semiring $\gamma$ and a family of additive commutative monoids $\beta_i$ indexed by $i \in \iota$, where each $\beta_i$ is equipped with a $\gamma$-module structure, the function `DFinsupp.filter p` is a $\gamma$-linear map from $\Pi₀ i, \beta_i$ to itself. Here, `p` is a decidable predicate on $\iota$, and the map acts by restricting a dependent function with finite support to the subset of indices where `p` holds, setting all other values to zero. More formally, for any $f \in \Pi₀ i, \beta_i$, the linear map is defined by: \[ (\text{DFinsupp.filterLinearMap } p)(f)(i) = \begin{cases} f(i) & \text{if } p(i) \text{ holds} \\ 0 & \text{otherwise} \end{cases} \]

DFinsupp.subtypeDomain_smul theorem

 [Monoid γ] [∀ i, AddMonoid (β i)] [∀ i, DistribMulAction γ (β i)] {p : ι → Prop} [DecidablePred p] (r : γ)
  (f : Π₀ i, β i) : (r • f).subtypeDomain p = r • f.subtypeDomain p

Full source

@[simp]
theorem subtypeDomain_smul [Monoid γ] [∀ i, AddMonoid (β i)] [∀ i, DistribMulAction γ (β i)]
    {p : ι → Prop} [DecidablePred p] (r : γ) (f : Π₀ i, β i) :
    (r • f).subtypeDomain p = r • f.subtypeDomain p :=
  DFunLike.coe_injective rfl

Scalar Multiplication Commutes with Restriction of Finitely Supported Functions

Informal description

Let $\gamma$ be a monoid, and let $\beta_i$ be a family of additive monoids indexed by $i \in \iota$, each equipped with a distributive multiplicative action by $\gamma$. For any predicate $p$ on $\iota$ (with decidable truth values) and any scalar $r \in \gamma$, the restriction of the scalar multiple $r \cdot f$ to the subtype defined by $p$ is equal to the scalar multiple of the restriction of $f$ to the same subtype. That is, $(r \cdot f)\big|_p = r \cdot (f\big|_p)$.

DFinsupp.subtypeDomainLinearMap definition

 [Semiring γ] [∀ i, AddCommMonoid (β i)] [∀ i, Module γ (β i)] (p : ι → Prop) [DecidablePred p] :
  (Π₀ i, β i) →ₗ[γ] Π₀ i : Subtype p, β i

Full source

/-- `DFinsupp.subtypeDomain` as a `LinearMap`. -/
@[simps]
def subtypeDomainLinearMap [Semiring γ] [∀ i, AddCommMonoid (β i)] [∀ i, Module γ (β i)]
    (p : ι → Prop) [DecidablePred p] : (Π₀ i, β i) →ₗ[γ] Π₀ i : Subtype p, β i where
  toFun := subtypeDomain p
  map_add' := subtypeDomain_add
  map_smul' := subtypeDomain_smul

Linear map of restriction to a subtype for finitely supported dependent functions

Informal description

Given a semiring $\gamma$, a family of additive commutative monoids $\beta_i$ indexed by $i \in \iota$ where each $\beta_i$ is a $\gamma$-module, and a decidable predicate $p$ on $\iota$, the function `subtypeDomain p` is a $\gamma$-linear map from the space of finitely supported dependent functions $\Pi₀ i, \beta i$ to the space of finitely supported dependent functions restricted to the subtype $\{i \in \iota \mid p(i)\}$. This map preserves addition and scalar multiplication, i.e., for any $f, g \in \Pi₀ i, \beta i$ and $c \in \gamma$, we have: - $\text{subtypeDomain}_p (f + g) = \text{subtypeDomain}_p f + \text{subtypeDomain}_p g$ - $\text{subtypeDomain}_p (c \cdot f) = c \cdot \text{subtypeDomain}_p f$

DFinsupp.mk_smul theorem

{s : Finset ι} (c : γ) (x : ∀ i : (↑s : Set ι), β (i : ι)) : mk s (c • x) = c • mk s x

Full source

@[simp]
theorem mk_smul {s : Finset ι} (c : γ) (x : ∀ i : (↑s : Set ι), β (i : ι)) :
    mk s (c • x) = c • mk s x :=
  ext fun i => by simp only [smul_apply, mk_apply]; split_ifs <;> [rfl; rw [smul_zero]]

Scalar Multiplication Commutes with Construction of Dependent Functions with Finite Support

Informal description

For any finite set $s$ of indices, any scalar $c$ in a monoid $\gamma$, and any function $x$ defined on $s$ (where for each $i \in s$, $x_i$ is an element of $\beta i$), the construction of a dependent function with finite support from the scalar multiple $c \cdot x$ is equal to the scalar multiple of the construction from $x$. That is, $\text{mk}_s (c \cdot x) = c \cdot \text{mk}_s x$.

DFinsupp.single_smul theorem

{i : ι} (c : γ) (x : β i) : single i (c • x) = c • single i x

Full source

@[simp]
theorem single_smul {i : ι} (c : γ) (x : β i) : single i (c • x) = c • single i x :=
  ext fun i => by
    simp only [smul_apply, single_apply]
    split_ifs with h
    · cases h; rfl
    · rw [smul_zero]

Scalar Multiplication Commutes with Kronecker Delta Function: $\text{single}_i(c \cdot x) = c \cdot \text{single}_i(x)$

Informal description

For any index $i$, scalar $c \in \gamma$, and element $x \in \beta_i$, the dependent Kronecker delta function $\text{single}_i(c \cdot x)$ is equal to the scalar multiple $c \cdot \text{single}_i(x)$.

DFinsupp.support_smul theorem

 {γ : Type w} [Semiring γ] [∀ i, AddCommMonoid (β i)] [∀ i, Module γ (β i)] [∀ (i : ι) (x : β i), Decidable (x ≠ 0)]
  (b : γ) (v : Π₀ i, β i) : (b • v).support ⊆ v.support

Full source

theorem support_smul {γ : Type w} [Semiring γ] [∀ i, AddCommMonoid (β i)] [∀ i, Module γ (β i)]
    [∀ (i : ι) (x : β i), Decidable (x ≠ 0)] (b : γ) (v : Π₀ i, β i) :
    (b • v).support ⊆ v.support :=
  support_mapRange

Support Inclusion Under Scalar Multiplication: $\text{supp}(b \cdot v) \subseteq \text{supp}(v)$

Informal description

Let $\gamma$ be a semiring, and let $\{\beta_i\}_{i \in \iota}$ be a family of additive commutative monoids indexed by $\iota$, each equipped with a $\gamma$-module structure. For any scalar $b \in \gamma$ and any dependent function $v \in \Pi_{i \in \iota} \beta_i$ with finite support, the support of the scalar multiple $b \cdot v$ is a subset of the support of $v$, i.e., \[ \text{supp}(b \cdot v) \subseteq \text{supp}(v). \]

DFinsupp.comapDomain_smul theorem

 [Monoid γ] [∀ i, AddMonoid (β i)] [∀ i, DistribMulAction γ (β i)] (h : κ → ι) (hh : Function.Injective h) (r : γ)
  (f : Π₀ i, β i) : comapDomain h hh (r • f) = r • comapDomain h hh f

Full source

@[simp]
theorem comapDomain_smul [Monoid γ] [∀ i, AddMonoid (β i)] [∀ i, DistribMulAction γ (β i)]
    (h : κ → ι) (hh : Function.Injective h) (r : γ) (f : Π₀ i, β i) :
    comapDomain h hh (r • f) = r • comapDomain h hh f := by
  ext
  rw [smul_apply, comapDomain_apply, smul_apply, comapDomain_apply]

Compatibility of Scalar Multiplication with Preimage in Dependent Finite Support Functions

Informal description

Let $\gamma$ be a monoid and $\{\beta_i\}_{i \in \iota}$ be a family of additive monoids, each equipped with a distributive multiplicative action by $\gamma$. For any injective function $h : \kappa \to \iota$, any scalar $r \in \gamma$, and any dependent function $f \in \Pi_{i \in \iota} \beta_i$ with finite support, the following equality holds: \[ \operatorname{comapDomain}\, h\, hh\, (r \cdot f) = r \cdot \operatorname{comapDomain}\, h\, hh\, f \] where $\operatorname{comapDomain}\, h\, hh\, f$ denotes the preimage of $f$ under $h$.

DFinsupp.comapDomain'_smul theorem

 [Monoid γ] [∀ i, AddMonoid (β i)] [∀ i, DistribMulAction γ (β i)] (h : κ → ι) {h' : ι → κ}
  (hh' : Function.LeftInverse h' h) (r : γ) (f : Π₀ i, β i) : comapDomain' h hh' (r • f) = r • comapDomain' h hh' f

Full source

@[simp]
theorem comapDomain'_smul [Monoid γ] [∀ i, AddMonoid (β i)] [∀ i, DistribMulAction γ (β i)]
    (h : κ → ι) {h' : ι → κ} (hh' : Function.LeftInverse h' h) (r : γ) (f : Π₀ i, β i) :
    comapDomain' h hh' (r • f) = r • comapDomain' h hh' f := by
  ext
  rw [smul_apply, comapDomain'_apply, smul_apply, comapDomain'_apply]

Scalar Multiplication Commutes with Precomposition in Dependent Finite Support Functions

Informal description

Let $\gamma$ be a monoid and $\{\beta_i\}_{i \in \iota}$ be a family of additive monoids, each equipped with a distributive multiplicative action by $\gamma$. Given a function $h \colon \kappa \to \iota$ with a left inverse $h' \colon \iota \to \kappa$ (i.e., $h'(h(k)) = k$ for all $k \in \kappa$), any scalar $r \in \gamma$, and any dependent function $f \in \Pi_{i \in \iota} \beta_i$ with finite support, we have \[ \operatorname{comapDomain}'\, h\, hh'\, (r \cdot f) = r \cdot \operatorname{comapDomain}'\, h\, hh'\, f, \] where $\operatorname{comapDomain}'\, h\, hh'\, f$ denotes the precomposition of $f$ with $h$.

DFinsupp.distribMulAction₂ instance

 [Monoid γ] [∀ i j, AddMonoid (δ i j)] [∀ i j, DistribMulAction γ (δ i j)] :
  DistribMulAction γ (Π₀ (i : ι) (j : α i), δ i j)

Full source

instance distribMulAction₂ [Monoid γ] [∀ i j, AddMonoid (δ i j)]
    [∀ i j, DistribMulAction γ (δ i j)] : DistribMulAction γ (Π₀ (i : ι) (j : α i), δ i j) :=
  @DFinsupp.distribMulAction ι _ (fun i => Π₀ j, δ i j) _ _ _

Pointwise Distributive Multiplicative Action on Doubly Dependent Functions with Finite Support

Informal description

For any monoid $\gamma$ and a family of additive monoids $\delta_{i,j}$ indexed by $i$ and $j$, where each $\delta_{i,j}$ is equipped with a distributive multiplicative action by $\gamma$, the type $\Pi₀ (i,j), \delta_{i,j}$ of doubly dependent functions with finite support inherits a distributive multiplicative action by $\gamma$ defined pointwise.

DFinsupp.equivProdDFinsupp_smul theorem

 [Monoid γ] [∀ i, AddMonoid (α i)] [∀ i, DistribMulAction γ (α i)] (r : γ) (f : Π₀ i, α i) :
  equivProdDFinsupp (r • f) = r • equivProdDFinsupp f

Full source

theorem equivProdDFinsupp_smul [Monoid γ] [∀ i, AddMonoid (α i)] [∀ i, DistribMulAction γ (α i)]
    (r : γ) (f : Π₀ i, α i) : equivProdDFinsupp (r • f) = r • equivProdDFinsupp f :=
  Prod.ext (smul_apply _ _ _) (comapDomain_smul _ (Option.some_injective _) _ _)

Equivariance of `equivProdDFinsupp` under scalar multiplication

Informal description

Let $\gamma$ be a monoid and $\{\alpha_i\}_{i \in \iota}$ be a family of additive monoids, each equipped with a distributive multiplicative action by $\gamma$. For any scalar $r \in \gamma$ and any dependent function $f \in \Pi_{i \in \iota} \alpha_i$ with finite support, the following equality holds: \[ \operatorname{equivProdDFinsupp}(r \cdot f) = r \cdot \operatorname{equivProdDFinsupp}(f), \] where $\operatorname{equivProdDFinsupp}$ is the bijection between $\Pi_{i \in \iota} \alpha_i$ and $\alpha_{\text{none}} \times \Pi_{i \in \iota} \alpha_{\text{some}(i)}$.

Main results