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
Instances For
    theorem Equiv.Perm.viaEmbedding_apply {α : Type u_1} {β : Type u_2} (e : Equiv.Perm α) (ι : α β) (x : α) :
    (e.viaEmbedding ι) (ι x) = ι (e x)
    theorem Equiv.Perm.viaEmbedding_apply_of_not_mem {α : Type u_1} {β : Type u_2} (e : Equiv.Perm α) (ι : α β) (x : β) (hx : xSet.range ι) :
    (e.viaEmbedding ι) x = x
    noncomputable def Equiv.Perm.viaEmbeddingHom {α : Type u_1} {β : Type u_2} (ι : α β) :

    viaEmbedding as a group homomorphism

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