# mathlib3documentation

algebra.smul_with_zero

# Introduce smul_with_zero#

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

In particular, for Types R and M, both containing 0, we define smul_with_zero 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 monoid_with_zero, we introduce the typeclass mul_action_with_zero 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 monoid_with_zero, acting as zero;
• associativity of the monoid.

We also add an instance:

• any monoid_with_zero has a mul_action_with_zero R R acting on itself.

## Main declarations #

• smul_monoid_with_zero_hom: Scalar multiplication bundled as a morphism of monoids with zero.
@[class]
structure smul_with_zero (R : Type u_1) (M : Type u_3) [has_zero R] [has_zero M] :
Type (max u_1 u_3)
• to_smul_zero_class :
• zero_smul : (m : M), 0 m = 0

smul_with_zero 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.

Instances of this typeclass
Instances of other typeclasses for smul_with_zero
• smul_with_zero.has_sizeof_inst
@[protected, instance]
Equations
@[protected, instance]

Like mul_zero_class.to_smul_with_zero, but multiplies on the right.

Equations
@[simp]
theorem zero_smul (R : Type u_1) {M : Type u_3} [has_zero R] [has_zero M] [ M] (m : M) :
0 m = 0
theorem smul_eq_zero_of_left {R : Type u_1} {M : Type u_3} [has_zero R] [has_zero M] [ M] {a : R} (h : a = 0) (b : M) :
a b = 0
theorem smul_eq_zero_of_right {R : Type u_1} {M : Type u_3} [has_zero R] [has_zero M] [ M] {b : M} (a : R) (h : b = 0) :
a b = 0
theorem left_ne_zero_of_smul {R : Type u_1} {M : Type u_3} [has_zero R] [has_zero M] [ M] {a : R} {b : M} :
a b 0 a 0
theorem right_ne_zero_of_smul {R : Type u_1} {M : Type u_3} [has_zero R] [has_zero M] [ M] {a : R} {b : M} :
a b 0 b 0
@[protected, reducible]
def function.injective.smul_with_zero {R : Type u_1} {M : Type u_3} {M' : Type u_4} [has_zero R] [has_zero M] [ M] [has_zero M'] [ M'] (f : zero_hom M' M) (hf : function.injective f) (smul : (a : R) (b : M'), f (a b) = a f b) :
M'

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

Equations
@[protected, reducible]
def function.surjective.smul_with_zero {R : Type u_1} {M : Type u_3} {M' : Type u_4} [has_zero R] [has_zero M] [ M] [has_zero M'] [ M'] (f : M') (hf : function.surjective f) (smul : (a : R) (b : M), f (a b) = a f b) :
M'

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

Equations
def smul_with_zero.comp_hom {R : Type u_1} {R' : Type u_2} (M : Type u_3) [has_zero R] [has_zero M] [ M] [has_zero R'] (f : zero_hom R' R) :
M

Compose a smul_with_zero with a zero_hom, with action f r' • m

Equations
@[protected, instance]
Equations
@[class]
structure mul_action_with_zero (R : Type u_1) (M : Type u_3) [has_zero M] :
Type (max u_1 u_3)
• to_mul_action : M
• smul_zero : (r : R), r 0 = 0
• zero_smul : (m : M), 0 m = 0

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

Instances of this typeclass
Instances of other typeclasses for mul_action_with_zero
• mul_action_with_zero.has_sizeof_inst
@[protected, instance]
def mul_action_with_zero.to_smul_with_zero (R : Type u_1) (M : Type u_3) [has_zero M] [m : M] :
Equations
@[protected, instance]

See also semiring.to_module

Equations
@[protected, instance]

Like monoid_with_zero.to_mul_action_with_zero, but multiplies on the right. See also semiring.to_opposite_module

Equations
@[protected]
theorem mul_action_with_zero.subsingleton (R : Type u_1) (M : Type u_3) [has_zero M] [ M] [subsingleton R] :
@[protected]
theorem mul_action_with_zero.nontrivial (R : Type u_1) (M : Type u_3) [has_zero M] [ M] [nontrivial M] :
@[protected, reducible]
def function.injective.mul_action_with_zero {R : Type u_1} {M : Type u_3} {M' : Type u_4} [has_zero M] [ M] [has_zero M'] [ M'] (f : zero_hom M' M) (hf : function.injective f) (smul : (a : R) (b : M'), f (a b) = a f b) :

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

Equations
@[protected, reducible]
def function.surjective.mul_action_with_zero {R : Type u_1} {M : Type u_3} {M' : Type u_4} [has_zero M] [ M] [has_zero M'] [ M'] (f : M') (hf : function.surjective f) (smul : (a : R) (b : M), f (a b) = a f b) :

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

Equations
def mul_action_with_zero.comp_hom {R : Type u_1} {R' : Type u_2} (M : Type u_3) [monoid_with_zero R'] [has_zero M] [ M] (f : R' →*₀ R) :

Compose a mul_action_with_zero with a monoid_with_zero_hom, with action f r' • m

Equations
theorem smul_inv₀ {α : Type u_5} {β : Type u_6} [ β] [ β] [ β] (c : α) (x : β) :
@[simp]
theorem smul_monoid_with_zero_hom_apply {α : Type u_1} {β : Type u_2} [ β] [ β] [ β] (ᾰ : α × β) :
def smul_monoid_with_zero_hom {α : Type u_1} {β : Type u_2} [ β] [ β] [ β] :
α × β →*₀ β

Scalar multiplication as a monoid homomorphism with zero.

Equations