Mathlib.Algebra.Module.Pi

IsSMulRegular.pi theorem

{α : Type*} [∀ i, SMul α <| f i] {k : α} (hk : ∀ i, IsSMulRegular (f i) k) : IsSMulRegular (∀ i, f i) k

Full source

theorem _root_.IsSMulRegular.pi {α : Type*} [∀ i, SMul α <| f i] {k : α}
    (hk : ∀ i, IsSMulRegular (f i) k) : IsSMulRegular (∀ i, f i) k := fun _ _ h =>
  funext fun i => hk i (congr_fun h i :)

Preservation of Left-Regularity in Product of Scalar Multiplications

Informal description

Let $\alpha$ be a type, and for each index $i$, suppose $f i$ has a scalar multiplication operation by $\alpha$. Given an element $k \in \alpha$ such that for each $i$, $k$ is left-regular (i.e., the map $x \mapsto k \cdot x$ is injective) on $f i$, then $k$ is also left-regular on the product type $\forall i, f i$.

Pi.smulWithZero instance

(α) [Zero α] [∀ i, Zero (f i)] [∀ i, SMulWithZero α (f i)] : SMulWithZero α (∀ i, f i)

Full source

instance smulWithZero (α) [Zero α] [∀ i, Zero (f i)] [∀ i, SMulWithZero α (f i)] :
    SMulWithZero α (∀ i, f i) :=
  { Pi.instSMul with
    smul_zero := fun _ => funext fun _ => smul_zero _
    zero_smul := fun _ => funext fun _ => zero_smul _ _ }

Scalar Multiplication with Zero on Product Types

Informal description

For any type $\alpha$ with a zero element and a family of types $f_i$ each with a zero element and a scalar multiplication operation $\alpha \times f_i \to f_i$ that preserves zero, the product type $\forall i, f_i$ inherits a scalar multiplication operation with zero from $\alpha$.

Pi.smulWithZero' instance

 {g : I → Type*} [∀ i, Zero (g i)] [∀ i, Zero (f i)] [∀ i, SMulWithZero (g i) (f i)] :
  SMulWithZero (∀ i, g i) (∀ i, f i)

Full source

instance smulWithZero' {g : I → Type*} [∀ i, Zero (g i)] [∀ i, Zero (f i)]
    [∀ i, SMulWithZero (g i) (f i)] : SMulWithZero (∀ i, g i) (∀ i, f i) :=
  { Pi.smul' with
    smul_zero := fun _ => funext fun _ => smul_zero _
    zero_smul := fun _ => funext fun _ => zero_smul _ _ }

Componentwise Scalar Multiplication with Zero on Product Types

Informal description

For any family of types $(g_i)$ and $(f_i)$ where each $g_i$ and $f_i$ has a zero element and each $g_i$ has a scalar multiplication operation on $f_i$ that preserves zero, the product type $\prod_i g_i$ has a scalar multiplication operation with zero on $\prod_i f_i$ defined componentwise.

Pi.mulActionWithZero instance

(α) [MonoidWithZero α] [∀ i, Zero (f i)] [∀ i, MulActionWithZero α (f i)] : MulActionWithZero α (∀ i, f i)

Full source

instance mulActionWithZero (α) [MonoidWithZero α] [∀ i, Zero (f i)]
    [∀ i, MulActionWithZero α (f i)] : MulActionWithZero α (∀ i, f i) :=
  { Pi.mulAction _, Pi.smulWithZero _ with }

Pointwise Multiplicative Action with Zero on Product Types

Informal description

For any monoid with zero $\alpha$ and a family of types $f_i$ each equipped with a zero element and a multiplicative action with zero of $\alpha$, the product type $\forall i, f_i$ (i.e., the type of functions from the index set $I$ to $\bigcup_i f_i$) inherits a multiplicative action with zero structure from $\alpha$, where the action is defined pointwise.

Pi.mulActionWithZero' instance

 {g : I → Type*} [∀ i, MonoidWithZero (g i)] [∀ i, Zero (f i)] [∀ i, MulActionWithZero (g i) (f i)] :
  MulActionWithZero (∀ i, g i) (∀ i, f i)

Full source

instance mulActionWithZero' {g : I → Type*} [∀ i, MonoidWithZero (g i)] [∀ i, Zero (f i)]
    [∀ i, MulActionWithZero (g i) (f i)] : MulActionWithZero (∀ i, g i) (∀ i, f i) :=
  { Pi.mulAction', Pi.smulWithZero' with }

Componentwise Multiplicative Action with Zero on Product Types

Informal description

For any family of monoids with zero $(g_i)$ and a family of types $(f_i)$ where each $f_i$ has a zero element and each $g_i$ has a multiplicative action with zero on $f_i$, the product type $\prod_i g_i$ has a multiplicative action with zero on $\prod_i f_i$ defined componentwise.

Pi.module instance

 (α) {r : Semiring α} {m : ∀ i, AddCommMonoid <| f i} [∀ i, Module α <| f i] :
  @Module α (∀ i : I, f i) r (@Pi.addCommMonoid I f m)

Full source

instance module (α) {r : Semiring α} {m : ∀ i, AddCommMonoid <| f i} [∀ i, Module α <| f i] :
    @Module α (∀ i : I, f i) r (@Pi.addCommMonoid I f m) :=
  { Pi.distribMulAction _ with
    add_smul := fun _ _ _ => funext fun _ => add_smul _ _ _
    zero_smul := fun _ => funext fun _ => zero_smul α _ }

Module Structure on Product Types with Pointwise Operations

Informal description

For any semiring $\alpha$ and a family of additive commutative monoids $(f_i)_{i \in I}$ where each $f_i$ is a module over $\alpha$, the product type $\prod_{i \in I} f_i$ is a module over $\alpha$ with pointwise operations.

Pi.Function.module instance

(α β : Type*) [Semiring α] [AddCommMonoid β] [Module α β] : Module α (I → β)

Full source

/-- A special case of `Pi.module` for non-dependent types. Lean struggles to elaborate
definitions elsewhere in the library without this. -/
instance Function.module (α β : Type*) [Semiring α] [AddCommMonoid β] [Module α β] :
    Module α (I → β) :=
  Pi.module _ _ _

Module Structure on Function Spaces with Pointwise Operations

Informal description

For any semiring $\alpha$, additive commutative monoid $\beta$, and module structure of $\alpha$ over $\beta$, the function space $I \to \beta$ is a module over $\alpha$ with pointwise operations.

Pi.module' instance

 {g : I → Type*} {r : ∀ i, Semiring (f i)} {m : ∀ i, AddCommMonoid (g i)} [∀ i, Module (f i) (g i)] :
  Module (∀ i, f i) (∀ i, g i)

Full source

instance module' {g : I → Type*} {r : ∀ i, Semiring (f i)} {m : ∀ i, AddCommMonoid (g i)}
    [∀ i, Module (f i) (g i)] : Module (∀ i, f i) (∀ i, g i) where
  add_smul := by
    intros
    ext1
    apply add_smul
  zero_smul := by
    intros
    ext1
    rw [zero_smul]

Module Structure on Product Types

Informal description

For an index type $I$ and families of semirings $(f_i)_{i \in I}$ and additive commutative monoids $(g_i)_{i \in I}$, if each $g_i$ is a module over $f_i$, then the product type $\prod_{i \in I} g_i$ is a module over the product semiring $\prod_{i \in I} f_i$.