# Introduce SMulWithZero#

In analogy with the usual monoid action on a Type M, we introduce an action of a MonoidWithZero on a Type with 0.

In particular, for Types R and M, both containing 0, we define SMulWithZero R M to be the typeclass where the products r • 0 and 0 • m vanish for all r : R and all m : M.

Moreover, in the case in which R is a MonoidWithZero, we introduce the typeclass MulActionWithZero R M, mimicking group actions and having an absorbing 0 in R. Thus, the action is required to be compatible with

• the unit of the monoid, acting as the identity;
• the zero of the MonoidWithZero, acting as zero;
• associativity of the monoid.

We also add an instance:

• any MonoidWithZero has a MulActionWithZero R R acting on itself.

## Main declarations #

• smulMonoidWithZeroHom: Scalar multiplication bundled as a morphism of monoids with zero.
class SMulWithZero (R : Type u_1) (M : Type u_3) [Zero R] [Zero M] extends :
Type (max u_1 u_3)

SMulWithZero is a class consisting of a Type R with 0 ∈ R and a scalar multiplication of R on a Type M with 0, such that the equality r • m = 0 holds if at least one among r or m equals 0.

• smul : RMM
• smul_zero : ∀ (a : R), a 0 = 0
• zero_smul : ∀ (m : M), 0 m = 0

Scalar multiplication by the scalar 0 is 0.

Instances
theorem SMulWithZero.zero_smul {R : Type u_1} {M : Type u_3} [Zero R] [Zero M] [self : ] (m : M) :
0 m = 0

Scalar multiplication by the scalar 0 is 0.

instance MulZeroClass.toSMulWithZero (R : Type u_1) [] :
Equations

Like MulZeroClass.toSMulWithZero, but multiplies on the right.

Equations
@[simp]
theorem zero_smul (R : Type u_1) {M : Type u_3} [Zero R] [Zero M] [] (m : M) :
0 m = 0
theorem smul_eq_zero_of_left {R : Type u_1} {M : Type u_3} [Zero R] [Zero M] [] {a : R} (h : a = 0) (b : M) :
a b = 0
theorem left_ne_zero_of_smul {R : Type u_1} {M : Type u_3} [Zero R] [Zero M] [] {a : R} {b : M} :
a b 0a 0
@[reducible, inline]
abbrev Function.Injective.smulWithZero {R : Type u_1} {M : Type u_3} {M' : Type u_4} [Zero R] [Zero M] [] [Zero M'] [SMul R M'] (f : ZeroHom M' M) (hf : ) (smul : ∀ (a : R) (b : M'), f (a b) = a f b) :

Pullback a SMulWithZero structure along an injective zero-preserving homomorphism. See note [reducible non-instances].

Equations
Instances For
@[reducible, inline]
abbrev Function.Surjective.smulWithZero {R : Type u_1} {M : Type u_3} {M' : Type u_4} [Zero R] [Zero M] [] [Zero M'] [SMul R M'] (f : ZeroHom M M') (hf : ) (smul : ∀ (a : R) (b : M), f (a b) = a f b) :

Pushforward a SMulWithZero structure along a surjective zero-preserving homomorphism. See note [reducible non-instances].

Equations
Instances For
def SMulWithZero.compHom {R : Type u_1} {R' : Type u_2} (M : Type u_3) [Zero R] [Zero M] [] [Zero R'] (f : ZeroHom R' R) :

Compose a SMulWithZero with a ZeroHom, with action f r' • m

Equations
Instances For
instance AddMonoid.natSMulWithZero {M : Type u_3} [] :
Equations
instance AddGroup.intSMulWithZero {M : Type u_3} [] :
Equations
class MulActionWithZero (R : Type u_1) (M : Type u_3) [] [Zero M] extends :
Type (max u_1 u_3)

An action of a monoid with zero R on a Type M, also with 0, extends MulAction and is compatible with 0 (both in R and in M), with 1 ∈ R, and with associativity of multiplication on the monoid M.

• smul : RMM
• one_smul : ∀ (b : M), 1 b = b
• mul_smul : ∀ (x y : R) (b : M), (x * y) b = x y b
• smul_zero : ∀ (r : R), r 0 = 0

Scalar multiplication by any element send 0 to 0.

• zero_smul : ∀ (m : M), 0 m = 0

Scalar multiplication by the scalar 0 is 0.

Instances
theorem MulActionWithZero.smul_zero {R : Type u_1} {M : Type u_3} [] [Zero M] [self : ] (r : R) :
r 0 = 0

Scalar multiplication by any element send 0 to 0.

theorem MulActionWithZero.zero_smul {R : Type u_1} {M : Type u_3} [] [Zero M] [self : ] (m : M) :
0 m = 0

Scalar multiplication by the scalar 0 is 0.

@[instance 100]
instance MulActionWithZero.toSMulWithZero (R : Type u_1) (M : Type u_3) [] [Zero M] [m : ] :
Equations

See also Semiring.toModule

Equations
• = let __src := ; let __src_1 := ;

Like MonoidWithZero.toMulActionWithZero, but multiplies on the right. See also Semiring.toOppositeModule

Equations
• = let __src := ; let __src_1 := Monoid.toOppositeMulAction;
theorem MulActionWithZero.subsingleton (R : Type u_1) (M : Type u_3) [] [Zero M] [] [] :
theorem MulActionWithZero.nontrivial (R : Type u_1) (M : Type u_3) [] [Zero M] [] [] :
theorem ite_zero_smul {R : Type u_1} {M : Type u_3} [] [Zero M] [] (p : Prop) [] (a : R) (b : M) :
(if p then a else 0) b = if p then a b else 0
theorem boole_smul {R : Type u_1} {M : Type u_3} [] [Zero M] [] (p : Prop) [] (a : M) :
(if p then 1 else 0) a = if p then a else 0
theorem Pi.single_apply_smul {R : Type u_1} {M : Type u_3} [] [Zero M] [] {ι : Type u_5} [] (x : M) (i : ι) (j : ι) :
Pi.single i 1 j x = Pi.single i x j
@[reducible, inline]
abbrev Function.Injective.mulActionWithZero {R : Type u_1} {M : Type u_3} {M' : Type u_4} [] [Zero M] [] [Zero M'] [SMul R M'] (f : ZeroHom M' M) (hf : ) (smul : ∀ (a : R) (b : M'), f (a b) = a f b) :

Pullback a MulActionWithZero structure along an injective zero-preserving homomorphism. See note [reducible non-instances].

Equations
Instances For
@[reducible, inline]
abbrev Function.Surjective.mulActionWithZero {R : Type u_1} {M : Type u_3} {M' : Type u_4} [] [Zero M] [] [Zero M'] [SMul R M'] (f : ZeroHom M M') (hf : ) (smul : ∀ (a : R) (b : M), f (a b) = a f b) :

Pushforward a MulActionWithZero structure along a surjective zero-preserving homomorphism. See note [reducible non-instances].

Equations
Instances For
def MulActionWithZero.compHom {R : Type u_1} {R' : Type u_2} (M : Type u_3) [] [] [Zero M] [] (f : R' →*₀ R) :

Compose a MulActionWithZero with a MonoidWithZeroHom, with action f r' • m

Equations
• = let __src := ;
Instances For
theorem smul_inv₀ {α : Type u_5} {β : Type u_6} [] [] [] [] [] (c : α) (x : β) :
@[simp]
theorem smulMonoidWithZeroHom_apply {α : Type u_5} {β : Type u_6} [] [] [] [] [] :
∀ (a : α × β), smulMonoidWithZeroHom a = (smulMonoidHom).toFun a
def smulMonoidWithZeroHom {α : Type u_5} {β : Type u_6} [] [] [] [] [] :
α × β →*₀ β

Scalar multiplication as a monoid homomorphism with zero.

Equations
• smulMonoidWithZeroHom = let __src := smulMonoidHom; { toFun := (__src).toFun, map_zero' := , map_one' := , map_mul' := }
Instances For
Equations
• NonUnitalNonAssocSemiring.toDistribSMul =