Mathlib.Algebra.Module.Prod

Module docstring

{"# Prod instances for module and multiplicative actions

This file defines instances for binary product of modules "}

Prod.smulWithZero instance

[Zero R] [Zero M] [Zero N] [SMulWithZero R M] [SMulWithZero R N] : SMulWithZero R (M × N)

Full source

instance smulWithZero [Zero R] [Zero M] [Zero N] [SMulWithZero R M] [SMulWithZero R N] :
    SMulWithZero R (M × N) where
  smul_zero _ := by ext <;> exact smul_zero ..
  zero_smul _ := by ext <;> exact zero_smul ..

Scalar Multiplication with Zero on Product Spaces

Informal description

For any type $R$ with a zero element, and types $M$ and $N$ each equipped with a zero element and a scalar multiplication operation `SMulWithZero R`, the product type $M \times N$ inherits a `SMulWithZero R` structure. This means that the scalar multiplication operation on $M \times N$ preserves the zero element and satisfies the usual compatibility conditions with addition and scalar multiplication.

Prod.mulActionWithZero instance

[MonoidWithZero R] [Zero M] [Zero N] [MulActionWithZero R M] [MulActionWithZero R N] : MulActionWithZero R (M × N)

Full source

instance mulActionWithZero [MonoidWithZero R] [Zero M] [Zero N] [MulActionWithZero R M]
    [MulActionWithZero R N] : MulActionWithZero R (M × N) :=
  { Prod.mulAction, Prod.smulWithZero with }

Componentwise Multiplicative Action with Zero on Product Types

Informal description

For any monoid with zero $R$ and types $M$ and $N$ each equipped with a zero element and a multiplicative action of $R$ that preserves zero, the product type $M \times N$ inherits a multiplicative action with zero structure from $R$ defined componentwise.

Prod.instModule instance

[Semiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] : Module R (M × N)

Full source

instance instModule [Semiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] :
    Module R (M × N) where
  add_smul _ _ _ := by ext <;> exact add_smul ..
  zero_smul _ := by ext <;> exact zero_smul ..

Module Structure on Product Spaces

Informal description

For any semiring $R$ and additive commutative monoids $M$ and $N$ that are modules over $R$, the product $M \times N$ is also a module over $R$ with componentwise operations.