Theorems · Definition · group theory

Function.Injective.addAction

{M : Type u_1} →
  {α : Type u_5} →
    {β : Type u_6} →
      [inst : AddMonoid M] →
        [inst_1 : AddAction M α] →
          [inst_2 : VAdd M β] →
            (f : β → α) → Function.Injective f → (∀ (c : M) (x : β), f (c +ᵥ x) = c +ᵥ f x) → AddAction M β

Pullback an additive action along an injective map respecting +ᵥ.

Defined in

Mathlib.Algebra.Group.Action.Defs

Cited by

0 results in Mathlib

Foundations

Depth 9 from the axioms · uses propext

Assumes

AddMonoidAddActionVAdd