Theorems · Definition · group theory

AddActionHom.zeroEmbeddingMap

{G : Type u_1} →
  {α : Type u_2} →
    [inst : AddGroup G] → [inst_1 : AddAction G α] → {zero : Type u_5} → [Unique zero] → (zero ↪ α) →ₑ[id] α

For Unique one, the equivariant map from one ↪ α to α

Defined in

Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Cited by

1 results in Mathlib

Foundations

Depth 18 from the axioms · uses propext, Quot.sound

Assumes

AddGroupAddActionUnique