theorem Hex.Perm.Cycle.Valid.fixed_of_dvd {n : Nat} {p : Perm n} {c : Array (Fin n)} (h : Valid p c) (k : Nat) (hk : c.size ∣ k) (x : Fin n) (hx : x ∈ c) : (p.pow k).get x = x

theorem Hex.Perm.Cycle.Valid.fixed_iff {n : Nat} {p : Perm n} {c : Array (Fin n)} (h : Valid p c) (x : Fin n) (hx : x ∈ c) : p.get x = x ↔ c.size = 1

theorem Hex.Perm.Cycle.lcm_fold_dvd {n : Nat} (cs : List (Array (Fin n))) (a k : Nat) : List.foldl (fun (j : Nat) (c : Array (Fin n)) => j.lcm c.size) a cs ∣ k ↔ a ∣ k ∧ ∀ (c : Array (Fin n)), c ∈ cs → c.size ∣ k

theorem Hex.Perm.Cycle.lcm_fold_pos {n : Nat} (cs : List (Array (Fin n))) (a : Nat) (ha : 0 < a) (hc : ∀ (c : Array (Fin n)), c ∈ cs → 0 < c.size) : 0 < List.foldl (fun (j : Nat) (c : Array (Fin n)) => j.lcm c.size) a cs

theorem Hex.Perm.cycles_valid {n : Nat} (p : Perm n) (c : Array (Fin n)) (hc : c ∈ p.cycles) : Cycle.Valid p c

theorem Hex.Perm.mem_cycles {n : Nat} (p : Perm n) (x : Fin n) : (∃ (c : Array (Fin n)), c ∈ p.cycles ∧ x ∈ c) ↔ p.get x ≠ x

The serialized nontrivial cycles contain precisely the moved points.

theorem Hex.Perm.cycles_ext {n : Nat} (p q : Perm n) (h : p.cycles = q.cycles) : p = q

The serialized nontrivial cycles determine the permutation uniquely; points absent from the serialization are fixed.

theorem Hex.Perm.order_pos {n : Nat} (p : Perm n) : 0 < p.order

theorem Hex.Perm.order_dvd_iff {n : Nat} (p : Perm n) (k : Nat) : p.order ∣ k ↔ ∀ (c : Array (Fin n)), c ∈ p.allCycles → c.size ∣ k

A number is a multiple of the computed order exactly when it is a multiple of every cycle length, including the omitted singleton cycles.

theorem Hex.Perm.order_dvd_iff_pow {n : Nat} (p : Perm n) (k : Nat) : p.order ∣ k ↔ p.pow k = Perm.id n

The lcm calculation recognizes exactly the exponents giving the identity.

theorem Hex.Perm.pow_order {n : Nat} (p : Perm n) : p.pow p.order = Perm.id n

theorem Hex.Perm.order_minimal {n : Nat} (p : Perm n) (k : Nat) (hk : 0 < k) (hp : p.pow k = Perm.id n) : p.order ≤ k

No positive exponent smaller than the computed order gives the identity.

theorem Hex.Perm.order_eq_one {n : Nat} (p : Perm n) : p.order = 1 ↔ p = Perm.id n