Injective map inducing perm group homomorphism

Stream: Is there code for X?

[Jordan Brown]

I want to use the fact that an injective map induces an inclusion of permutation groups; the case where the map is inclusion of a subtype already seems to be in mathlib, but I cannot find the result for an arbitrary injective map. Is it in mathlib yet, or do I need to prove it?

[Yakov Pechersky]

Something like

def equiv.perm.of_embedding {α β : Type*} [fintype α] [decidable_eq β]
  (e : equiv.perm α) (f : α ↪ β) : equiv.perm β :=
equiv.perm.subtype_congr (e.of_embedding_subtype f) (equiv.refl _)