Extra lemmas about permutations

This file proves miscellaneous lemmas about Equiv.Perm.

TODO

Most of the content of this file was moved to Mathlib/Algebra/Group/End.lean in https://github.com/leanprover-community/mathlib4/pull/22141. It would be good to merge the remaining lemmas with other files, e.g. GroupTheory.Perm.ViaEmbedding looks like it could benefit from such a treatment (splitting into the algebra and non-algebra parts).

@[deprecated Equiv.image_symm_eq_preimage (since := "2025-08-16")]

theorem Equiv.Perm.image_inv {α : Type u} (f : Perm α) (s : Set α) : ⇑f⁻¹ '' s = ⇑f ⁻¹' s

@[deprecated Equiv.image_eq_preimage_symm (since := "2025-08-16")]

theorem Equiv.Perm.preimage_inv {α : Type u} (f : Perm α) (s : Set α) : ⇑f⁻¹ ⁻¹' s = ⇑f '' s

@[simp]

theorem Equiv.swap_smul_self_smul {α : Type u} {β : Type v} [DecidableEq α] [MulAction (Perm α) β] (i j : α) (x : β) : swap i j • swap i j • x = x

theorem Equiv.swap_smul_involutive {α : Type u} {β : Type v} [DecidableEq α] [MulAction (Perm α) β] (i j : α) : Function.Involutive fun (x : β) => swap i j • x

theorem Set.BijOn.perm_inv {α : Type u_1} {f : Equiv.Perm α} {s : Set α} (hf : BijOn (⇑f) s s) : BijOn (⇑f⁻¹) s s

theorem Set.MapsTo.perm_pow {α : Type u_1} {f : Equiv.Perm α} {s : Set α} : MapsTo (⇑f) s s → ∀ (n : ℕ), MapsTo (⇑(f ^ n)) s s

theorem Set.SurjOn.perm_pow {α : Type u_1} {f : Equiv.Perm α} {s : Set α} : SurjOn (⇑f) s s → ∀ (n : ℕ), SurjOn (⇑(f ^ n)) s s

theorem Set.BijOn.perm_pow {α : Type u_1} {f : Equiv.Perm α} {s : Set α} : BijOn (⇑f) s s → ∀ (n : ℕ), BijOn (⇑(f ^ n)) s s

theorem Set.BijOn.perm_zpow {α : Type u_1} {f : Equiv.Perm α} {s : Set α} (hf : BijOn (⇑f) s s) (n : ℤ) : BijOn (⇑(f ^ n)) s s