α : Type u
β : Type v
p : α → Prop
f : Perm α
hf : ∀ (x : α), p x ↔ p (↑f x)
n : ℕ
⊢ ∀ (x : α), p x ↔ p (↑(f ^ (n + 1))⁻¹ x)
α : Type u
β : Type v
p : α → Prop
f : Perm α
hf : ∀ (x : α), p x ↔ p (↑f x)
n : ℕ
⊢ ∀ (x : α), p x ↔ p (↑(f ^ Int.negSucc n) x)
rw [zpow_negSucc]
no goals
α : Type u
β : Type v
p : α → Prop
f : Perm α
hf : ∀ (x : α), p x ↔ p (↑f x)
n : ℕ
⊢ ∀ (x : α), p x ↔ p (↑(f ^ (n + 1))⁻¹ x)
exact inv_aux.1 (pow_aux hf)