Extra lemmas about periodic points

theorem Function.directed_ptsOfPeriod_pNat {α : Type u_1} (f : α → α) : Directed (fun (x1 x2 : Set α) => x1 ⊆ x2) fun (n : ℕ+) => ptsOfPeriod f ↑n

theorem Function.bijOn_periodicPts {α : Type u_1} (f : α → α) : Set.BijOn f (periodicPts f) (periodicPts f)

theorem Function.minimalPeriod_eq_prime {α : Type u_1} {f : α → α} {x : α} {p : ℕ} [hp : Fact (Nat.Prime p)] (hper : IsPeriodicPt f p x) (hfix : ¬IsFixedPt f x) : minimalPeriod f x = p

theorem Function.minimalPeriod_eq_prime_pow {α : Type u_1} {f : α → α} {x : α} {p k : ℕ} [hp : Fact (Nat.Prime p)] (hk : ¬IsPeriodicPt f (p ^ k) x) (hk1 : IsPeriodicPt f (p ^ (k + 1)) x) : minimalPeriod f x = p ^ (k + 1)

theorem Function.Commute.minimalPeriod_of_comp_dvd_mul {α : Type u_1} {f : α → α} {x : α} {g : α → α} (h : Function.Commute f g) : minimalPeriod (f ∘ g) x ∣ minimalPeriod f x * minimalPeriod g x

theorem Function.Commute.minimalPeriod_of_comp_eq_mul_of_coprime {α : Type u_1} {f : α → α} {x : α} {g : α → α} (h : Function.Commute f g) (hco : (minimalPeriod f x).Coprime (minimalPeriod g x)) : minimalPeriod (f ∘ g) x = minimalPeriod f x * minimalPeriod g x

theorem Function.minimalPeriod_prod_map {α : Type u_1} {β : Type u_2} (f : α → α) (g : β → β) (x : α × β) : minimalPeriod (Prod.map f g) x = (minimalPeriod f x.1).lcm (minimalPeriod g x.2)

theorem Function.minimalPeriod_fst_dvd {α : Type u_1} {β : Type u_2} {f : α → α} {g : β → β} {x : α × β} : minimalPeriod f x.1 ∣ minimalPeriod (Prod.map f g) x

theorem Function.minimalPeriod_snd_dvd {α : Type u_1} {β : Type u_2} {f : α → α} {g : β → β} {x : α × β} : minimalPeriod g x.2 ∣ minimalPeriod (Prod.map f g) x