Theorems · Definition · group theory

MulDistribMulAction.toMulEquiv

{G : Type u_1} → (M : Type u_2) → [inst : Group G] → [inst_1 : Monoid M] → [MulDistribMulAction G M] → G → M ≃* M

Each element of the group defines a multiplicative monoid isomorphism. This is a stronger version of MulAction.toPerm.

Defined in

Mathlib.Algebra.Group.Action.End

Cited by

5 results in Mathlib

Foundations

Depth 23 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupMonoidMulDistribMulAction