Theorems · Definition · group theory

MulDistribMulAction.toMonoidHom

{M : Type u_2} → (A : Type u_3) → [inst : Monoid M] → [inst_1 : Monoid A] → [MulDistribMulAction M A] → M → A →* A

Scalar multiplication by r as a MonoidHom.

Defined in

Mathlib.Algebra.Group.Action.Basic

Cited by

10 results in Mathlib

Foundations

Depth 8 from the axioms · uses no axioms

Assumes

MonoidMonoidMulDistribMulAction