mathlib3 documentation

group_theory.perm.via_embedding

equiv.perm.via_embedding, a noncomputable analogue of equiv.perm.via_fintype_embedding. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

noncomputable def equiv.perm.via_embedding {α : Type u_1} {β : Type u_2} (e : equiv.perm α) (ι : α β) :

Noncomputable version of equiv.perm.via_fintype_embedding that does not assume fintype

Equations
theorem equiv.perm.via_embedding_apply {α : Type u_1} {β : Type u_2} (e : equiv.perm α) (ι : α β) (x : α) :
(e.via_embedding ι) (ι x) = ι (e x)
theorem equiv.perm.via_embedding_apply_of_not_mem {α : Type u_1} {β : Type u_2} (e : equiv.perm α) (ι : α β) (x : β) (hx : x set.range ι) :
(e.via_embedding ι) x = x
noncomputable def equiv.perm.via_embedding_hom {α : Type u_1} {β : Type u_2} (ι : α β) :

via_embedding as a group homomorphism

Equations
theorem equiv.perm.via_embedding_hom_apply {α : Type u_1} {β : Type u_2} (e : equiv.perm α) (ι : α β) :