Equiv.Perm.viaEmbedding, a noncomputable analogue of Equiv.Perm.viaFintypeEmbedding.

noncomputable def Equiv.Perm.viaEmbedding {α : Type u_1} {β : Type u_2} (e : Perm α) (ι : α ↪ β) : Perm β

Noncomputable version of Equiv.Perm.viaFintypeEmbedding that does not assume Fintype

theorem Equiv.Perm.viaEmbedding_apply {α : Type u_1} {β : Type u_2} (e : Perm α) (ι : α ↪ β) (x : α) : (e.viaEmbedding ι) (ι x) = ι (e x)

theorem Equiv.Perm.viaEmbedding_apply_of_notMem {α : Type u_1} {β : Type u_2} (e : Perm α) (ι : α ↪ β) (x : β) (hx : x ∉ Set.range ⇑ι) : (e.viaEmbedding ι) x = x

@[deprecated Equiv.Perm.viaEmbedding_apply_of_notMem (since := "2025-05-23")]

theorem Equiv.Perm.viaEmbedding_apply_of_not_mem {α : Type u_1} {β : Type u_2} (e : Perm α) (ι : α ↪ β) (x : β) (hx : x ∉ Set.range ⇑ι) : (e.viaEmbedding ι) x = x

Alias of Equiv.Perm.viaEmbedding_apply_of_notMem.

noncomputable def Equiv.Perm.viaEmbeddingHom {α : Type u_1} {β : Type u_2} (ι : α ↪ β) : Perm α →* Perm β

viaEmbedding as a group homomorphism

theorem Equiv.Perm.viaEmbeddingHom_apply {α : Type u_1} {β : Type u_2} (e : Perm α) (ι : α ↪ β) : (viaEmbeddingHom ι) e = e.viaEmbedding ι

theorem Equiv.Perm.viaEmbeddingHom_injective {α : Type u_1} {β : Type u_2} (ι : α ↪ β) : Function.Injective ⇑(viaEmbeddingHom ι)