Documentation

Mathlib.GroupTheory.Perm.ViaEmbedding

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

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

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

Equations
theorem Equiv.Perm.viaEmbedding_apply {α : Type u_2} {β : Type u_1} (e : Equiv.Perm α) (ι : α β) (x : α) :
↑(Equiv.Perm.viaEmbedding e ι) (ι x) = ι (e x)
theorem Equiv.Perm.viaEmbedding_apply_of_not_mem {α : Type u_2} {β : Type u_1} (e : Equiv.Perm α) (ι : α β) (x : β) (hx : ¬x Set.range ι) :
noncomputable def Equiv.Perm.viaEmbeddingHom {α : Type u_1} {β : Type u_2} (ι : α β) :

viaEmbedding as a group homomorphism

Equations
theorem Equiv.Perm.viaEmbeddingHom_apply {α : Type u_2} {β : Type u_1} (e : Equiv.Perm α) (ι : α β) :