Theorems · Definition · group theory

Function.Injective.mulAction

{M : Type u_1} →
  {α : Type u_5} →
    {β : Type u_6} →
      [inst : Monoid M] →
        [inst_1 : MulAction M α] →
          [inst_2 : SMul M β] →
            (f : β → α) → Function.Injective f → (∀ (c : M) (x : β), f (c • x) = c • f x) → MulAction M β

Pullback a multiplicative action along an injective map respecting •. See note [reducible non-instances].

Defined in

Mathlib.Algebra.Group.Action.Defs

Cited by

0 results in Mathlib

Foundations

Depth 9 from the axioms · uses propext

Assumes

MonoidMulActionSMul