Theorems · Definition · group theory

DistribSMul.toAddMonoidHom

{M : Type u_1} → (A : Type u_7) → [inst : AddZeroClass A] → [DistribSMul M A] → M → A →+ A

Each element of the scalars defines an additive monoid homomorphism.

Defined in

Mathlib.Algebra.GroupWithZero.Action.Defs

Cited by

20 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms

Assumes

AddZeroClassDistribSMul