`BookProof.ChapterA3u.invariant_sameCycle` {N : ℕ} {σ : Equiv.Perm (Fin N)} {a : Idx N} (ha : a ∘ σ = a) {x y : Fin N} (h : σ.SameCycle x y) : a x = a y

Initializing...

`BookProof.ChapterA3u.invariant_sameCycle` {N : ℕ} {σ : Equiv.Perm (Fin N)} {a : Idx N} (ha : a ∘ σ = a) {x y : Fin N} (h : σ.SameCycle x y) : a x = a y · Prove2Me