Theorems · Theorem · group theory

Equiv.Perm.exists_smul_eq_embedding

∀ {ι : Type u_2} [Finite ι] {β : Type u_3} (x y : ι ↪ β), ∃ σ, σ • x = y

For any two embeddings from a finite type into β, some permutation of β maps one to the other. This is the action-form of Equiv.Perm.exists_extending_pair.

Defined in

Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Cited by

1 results in Mathlib

Foundations

Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Finite