ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>τ : Type u_1<VAR>TopologicalSpace τ<VAR>AddCommGroup τ<VAR>TopologicalAddGroup τ<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>f : Filter τ<VAR>ϕ : Flow τ α<VAR>s : Set α<VAR>hf : ∀ (t : τ), Filter.Tendsto (fun x => x + t) f f<VAR>t : τ<GOAL>omegaLimit f ϕ.toFun (ϕ.toFun t '' s) = omegaLimit f ϕ.toFun s
<VAR>τ : Type u_1<VAR>TopologicalSpace τ<VAR>AddCommGroup τ<VAR>TopologicalAddGroup τ<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>f : Filter τ<VAR>ϕ : Flow τ α<VAR>s : Set α<VAR>hf : ∀ (t : τ), Filter.Tendsto (fun x => t + x) f f<GOAL>omegaLimit f ϕ.toFun (omegaLimit f ϕ.toFun s) ⊆ omegaLimit f ϕ.toFun s
<VAR>R : Type u_2<VAR>CommRing R<VAR>IsDomain R<VAR>DecidableEq R<VAR>Fintype R<VAR>p : R[X]<VAR>hp : 0 < p.degree<GOAL>Fintype.card R ≤ p.natDegree * (Finset.image (fun x => Polynomial.eval x p) Finset.univ).card
<VAR>R : Type u_2<VAR>CommRing R<VAR>IsDomain R<VAR>Fintype R<VAR>f g : R[X]<VAR>hf2 : f.degree = 2<VAR>hg2 : g.degree = 2<VAR>hR : Fintype.card R % 2 = 1<GOAL>∃ a b, Polynomial.eval a f + Polynomial.eval b g = 0
<VAR>K : Type u_1<VAR>CommRing K<VAR>IsDomain K<VAR>Fintype Kˣ<GOAL>∏ x : Kˣ, x = -1
<VAR>K : Type u_1<VAR>Ring K<VAR>NoZeroDivisors K<VAR>Nontrivial K<VAR>G : Subgroup Kˣ<VAR>Fintype ↥G<GOAL>↑(Fintype.card ↥G) ≠ 0
<VAR>K : Type u_1<VAR>Ring K<VAR>NoZeroDivisors K<VAR>G : Subgroup Kˣ<VAR>Fintype ↥G<VAR>hg : G ≠ ⊥<GOAL>∑ x : ↥G, ↑↑x = 0
<VAR>K : Type u_1<VAR>Ring K<VAR>NoZeroDivisors K<VAR>G : Subgroup Kˣ<VAR>Fintype ↥G<VAR>Decidable (G = ⊥)<GOAL>∑ x : ↥G, ↑↑x = if G = ⊥ then 1 else 0
<VAR>K : Type u_1<VAR>CommRing K<VAR>NoZeroDivisors K<VAR>G : Subgroup Kˣ<VAR>Fintype ↥G<VAR>k : ℕ<VAR>k_pos : k ≠ 0<VAR>k_lt_card_G : k < Fintype.card ↥G<GOAL>∑ x : ↥G, ↑↑x ^ k = 0
<VAR>K : Type u_1<VAR>GroupWithZero K<VAR>Fintype K<VAR>a : K<VAR>ha : a ≠ 0<GOAL>a ^ (q - 1) = 1
<VAR>K : Type u_1<VAR>GroupWithZero K<VAR>Fintype K<VAR>a : K<GOAL>a ^ q = a
<VAR>K : Type u_1<VAR>GroupWithZero K<VAR>Fintype K<VAR>n : ℕ<VAR>a : K<GOAL>a ^ q ^ n = a
<VAR>K : Type u_1<VAR>Field K<VAR>Fintype K<VAR>p : ℕ<VAR>CharP K p<GOAL>∃ n, Nat.Prime p ∧ q = p ^ ↑n
<VAR>K : Type u_1<VAR>Field K<VAR>Fintype K<GOAL>∃ p n, Nat.Prime p ∧ q = p ^ ↑n
<VAR>K : Type u_1<VAR>Field K<VAR>Fintype K<GOAL>↑q = 0
<VAR>K : Type u_1<VAR>Field K<VAR>Fintype K<VAR>i : ℕ<GOAL>(∀ (x : Kˣ), x ^ i = 1) ↔ q - 1 ∣ i
<VAR>K : Type u_1<VAR>Field K<VAR>Fintype K<VAR>DecidableEq K<VAR>i : ℕ<GOAL>∑ x : Kˣ, ↑x ^ i = if q - 1 ∣ i then -1 else 0
<VAR>K : Type u_1<VAR>Field K<VAR>Fintype K<VAR>i : ℕ<VAR>h : i < q - 1<GOAL>∑ x : K, x ^ i = 0
<VAR>K' : Type u_3<VAR>Field K'<VAR>p : ℕ<VAR>hp : 1 < p<GOAL>(Polynomial.X ^ p - Polynomial.X).natDegree = p
<VAR>K' : Type u_3<VAR>Field K'<VAR>p n : ℕ<VAR>hn : n ≠ 0<VAR>hp : 1 < p<GOAL>(Polynomial.X ^ p ^ n - Polynomial.X).natDegree = p ^ n
<VAR>K' : Type u_3<VAR>Field K'<VAR>p : ℕ<VAR>hp : 1 < p<GOAL>Polynomial.X ^ p - Polynomial.X ≠ 0
<VAR>K' : Type u_3<VAR>Field K'<VAR>p n : ℕ<VAR>hn : n ≠ 0<VAR>hp : 1 < p<GOAL>Polynomial.X ^ p ^ n - Polynomial.X ≠ 0
<VAR>K : Type u_1<VAR>Field K<VAR>Fintype K<GOAL>(Polynomial.X ^ q - Polynomial.X).roots = Finset.univ.val
<VAR>K : Type u_1<VAR>Field K<VAR>Fintype K<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>CharP K p<VAR>n : ℕ<VAR>hcard : q = p ^ n<GOAL>frobenius K p ^ n = 1
<VAR>K : Type u_1<VAR>Field K<VAR>Fintype K<VAR>f : K[X]<GOAL>(Polynomial.expand K q) f = f ^ q
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ZMod p<GOAL>∃ a b, a ^ 2 + b ^ 2 = x
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>x : ℤ<GOAL>∃ a b, a ≤ p / 2 ∧ b ≤ p / 2 ∧ ↑a ^ 2 + ↑b ^ 2 ≡ x [ZMOD ↑p]
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>x : ℕ<GOAL>∃ a b, a ≤ p / 2 ∧ b ≤ p / 2 ∧ a ^ 2 + b ^ 2 ≡ x [MOD p]
<VAR>R : Type u_3<VAR>CommRing R<VAR>IsDomain R<VAR>p : ℕ<VAR>NeZero p<VAR>CharP R p<VAR>x : ℤ<GOAL>∃ a b, ↑a ^ 2 + ↑b ^ 2 = ↑x
<VAR>n : ℕ<VAR>x : (ZMod n)ˣ<GOAL>x ^ φ n = 1
<VAR>x n : ℕ<VAR>h : x.Coprime n<GOAL>x ^ φ n ≡ 1 [MOD n]
<VAR>K : Type u_1<VAR>V : Type u_3<VAR>Fintype K<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>Fintype V<GOAL>Fintype.card V = q ^ FiniteDimensional.finrank K V
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>x : ZMod p<GOAL>x ^ p = x
<VAR>n p : ℕ<VAR>Fact (Nat.Prime p)<VAR>x : ZMod p<GOAL>x ^ p ^ n = x
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<GOAL>frobenius (ZMod p) p = RingHom.id (ZMod p)
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<GOAL>Fintype.card (ZMod p)ˣ = p - 1
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>a : (ZMod p)ˣ<GOAL>a ^ (p - 1) = 1
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>a : ZMod p<VAR>ha : a ≠ 0<GOAL>a ^ (p - 1) = 1
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>a : ZMod p<GOAL>a ^ (p - 1) = if a ≠ 0 then 1 else 0
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>u : (ZMod p)ˣ<GOAL>orderOf u ∣ p - 1
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>a : ZMod p<VAR>ha : a ≠ 0<GOAL>orderOf a ∣ p - 1
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>f : (ZMod p)[X]<GOAL>(Polynomial.expand (ZMod p) p) f = f ^ p
<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>n : ℤ<VAR>hpn : IsCoprime n ↑p<GOAL>n ^ (p - 1) ≡ 1 [ZMOD ↑p]
<VAR>F : Type u_3<VAR>Field F<VAR>Finite F<VAR>hF : ringChar F = 2<VAR>a : F<GOAL>IsSquare a
<VAR>F : Type u_3<VAR>Field F<VAR>Finite F<VAR>hF : ringChar F ≠ 2<GOAL>∃ a, ¬IsSquare a
<VAR>F : Type u_3<VAR>Field F<VAR>Fintype F<GOAL>ringChar F = 2 ↔ Fintype.card F % 2 = 0
<VAR>F : Type u_3<VAR>Field F<VAR>Fintype F<VAR>hF : ringChar F = 2<GOAL>Fintype.card F % 2 = 0
<VAR>F : Type u_3<VAR>Field F<VAR>Fintype F<VAR>hF : ringChar F ≠ 2<GOAL>Fintype.card F % 2 = 1
<VAR>F : Type u_3<VAR>Field F<VAR>Fintype F<VAR>hF : ringChar F ≠ 2<VAR>a : F<VAR>ha : a ≠ 0<GOAL>a ^ (Fintype.card F / 2) = 1 ∨ a ^ (Fintype.card F / 2) = -1
<VAR>F : Type u_3<VAR>Field F<VAR>Fintype F<VAR>hF : ringChar F ≠ 2<VAR>a : Fˣ<GOAL>IsSquare a ↔ a ^ (Fintype.card F / 2) = 1
<VAR>F : Type u_3<VAR>Field F<VAR>Fintype F<VAR>hF : ringChar F ≠ 2<VAR>a : F<VAR>ha : a ≠ 0<GOAL>IsSquare a ↔ a ^ (Fintype.card F / 2) = 1
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<VAR>hf : Function.IsFixedPt f x<VAR>n : ℕ<GOAL>Function.IsPeriodicPt f n x
<VAR>α : Type u_1<VAR>n : ℕ<VAR>x : α<GOAL>Function.IsPeriodicPt id n x
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<GOAL>Function.IsPeriodicPt f 0 x
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<VAR>n : ℕ<VAR>hf : Function.IsPeriodicPt f n x<GOAL>Function.IsFixedPt f^[n] x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>fa : α → α<VAR>fb : β → β<VAR>x : α<VAR>n : ℕ<VAR>hx : Function.IsPeriodicPt fa n x<VAR>g : α → β<VAR>hg : Function.Semiconj g fa fb<GOAL>Function.IsPeriodicPt fb n (g x)
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<VAR>n : ℕ<VAR>hx : Function.IsPeriodicPt f n x<VAR>m : ℕ<GOAL>Function.IsPeriodicPt f n (f^[m] x)
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<VAR>n : ℕ<VAR>hx : Function.IsPeriodicPt f n x<GOAL>Function.IsPeriodicPt f n (f x)
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<VAR>m n : ℕ<VAR>hn : Function.IsPeriodicPt f n x<VAR>hm : Function.IsPeriodicPt f m x<GOAL>Function.IsPeriodicPt f (n + m) x
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<VAR>m n : ℕ<VAR>hn : Function.IsPeriodicPt f (n + m) x<VAR>hm : Function.IsPeriodicPt f m x<GOAL>Function.IsPeriodicPt f n x
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<VAR>m n : ℕ<VAR>hn : Function.IsPeriodicPt f (n + m) x<VAR>hm : Function.IsPeriodicPt f n x<GOAL>Function.IsPeriodicPt f m x
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<VAR>m n : ℕ<VAR>hm : Function.IsPeriodicPt f m x<VAR>hn : Function.IsPeriodicPt f n x<GOAL>Function.IsPeriodicPt f (m - n) x
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<VAR>m : ℕ<VAR>hm : Function.IsPeriodicPt f m x<VAR>n : ℕ<GOAL>Function.IsPeriodicPt f (m * n) x
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<VAR>m : ℕ<VAR>hm : Function.IsPeriodicPt f m x<VAR>n : ℕ<GOAL>Function.IsPeriodicPt f (n * m) x
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<VAR>m : ℕ<VAR>hm : Function.IsPeriodicPt f m x<VAR>n : ℕ<VAR>hn : m ∣ n<GOAL>Function.IsPeriodicPt f n x
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<VAR>n : ℕ<VAR>hf : Function.IsPeriodicPt f n x<VAR>m : ℕ<GOAL>Function.IsPeriodicPt f^[m] n x
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<VAR>n : ℕ<VAR>g : α → α<VAR>hco : Function.Commute f g<VAR>hf : Function.IsPeriodicPt f n x<VAR>hg : Function.IsPeriodicPt g n x<GOAL>Function.IsPeriodicPt (f ∘ g) n x
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<VAR>m n : ℕ<VAR>g : α → α<VAR>hco : Function.Commute f g<VAR>hf : Function.IsPeriodicPt f m x<VAR>hg : Function.IsPeriodicPt g n x<GOAL>Function.IsPeriodicPt (f ∘ g) (m.lcm n) x
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<VAR>n : ℕ<VAR>g : α → α<VAR>hco : Function.Commute f g<VAR>hfg : Function.IsPeriodicPt (f ∘ g) n x<VAR>hg : Function.IsPeriodicPt g n x<GOAL>Function.IsPeriodicPt f n x
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<VAR>n : ℕ<VAR>h : Function.IsPeriodicPt f n x<VAR>m : ℕ<GOAL>f^[m % n] x = f^[m] x
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<VAR>m n : ℕ<VAR>hm : Function.IsPeriodicPt f m x<VAR>hn : Function.IsPeriodicPt f n x<GOAL>Function.IsPeriodicPt f (m % n) x
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<VAR>m n : ℕ<VAR>hm : Function.IsPeriodicPt f m x<VAR>hn : Function.IsPeriodicPt f n x<GOAL>Function.IsPeriodicPt f (m.gcd n) x
<VAR>α : Type u_1<VAR>f : α → α<VAR>x y : α<VAR>n : ℕ<VAR>hx : Function.IsPeriodicPt f n x<VAR>hy : Function.IsPeriodicPt f n y<VAR>hn : 0 < n<VAR>h : f x = f y<GOAL>x = y
<VAR>α : Type u_1<VAR>f : α → α<VAR>x y : α<VAR>m n : ℕ<VAR>hx : Function.IsPeriodicPt f m x<VAR>hy : Function.IsPeriodicPt f n y<VAR>hm : 0 < m<VAR>hn : 0 < n<VAR>h : f x = f y<GOAL>x = y
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<VAR>n : ℕ<GOAL>x ∈ Function.ptsOfPeriod f n ↔ Function.IsPeriodicPt f n x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>fa : α → α<VAR>fb : β → β<VAR>g : α → β<VAR>h : Function.Semiconj g fa fb<VAR>n : ℕ<GOAL>Set.MapsTo g (Function.ptsOfPeriod fa n) (Function.ptsOfPeriod fb n)
<VAR>α : Type u_1<VAR>f : α → α<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>Set.BijOn f (Function.ptsOfPeriod f n) (Function.ptsOfPeriod f n)
<VAR>α : Type u_1<VAR>f : α → α<GOAL>Directed (fun x x_1 => x ⊆ x_1) fun n => Function.ptsOfPeriod f ↑n
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<VAR>n : ℕ<VAR>hn : 0 < n<VAR>hx : Function.IsPeriodicPt f n x<GOAL>x ∈ Function.periodicPts f
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<GOAL>x ∈ Function.periodicPts f ↔ ∃ n > 0, Function.IsPeriodicPt f n x
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<VAR>m n : ℕ<VAR>hx : x ∈ Function.periodicPts f<VAR>hm : Function.IsPeriodicPt f m (f^[n] x)<GOAL>Function.IsPeriodicPt f m x
<VAR>α : Type u_1<VAR>f : α → α<GOAL>⋃ n, ⋃ (_ : n > 0), Function.ptsOfPeriod f n = Function.periodicPts f
<VAR>α : Type u_1<VAR>f : α → α<GOAL>⋃ n, Function.ptsOfPeriod f ↑n = Function.periodicPts f
<VAR>α : Type u_1<VAR>f : α → α<GOAL>Set.BijOn f (Function.periodicPts f) (Function.periodicPts f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>fa : α → α<VAR>fb : β → β<VAR>g : α → β<VAR>h : Function.Semiconj g fa fb<GOAL>Set.MapsTo g (Function.periodicPts fa) (Function.periodicPts fb)
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<GOAL>Function.IsPeriodicPt f (Function.minimalPeriod f x) x
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<GOAL>f^[Function.minimalPeriod f x] x = x
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<VAR>n : ℕ<GOAL>f^[n + Function.minimalPeriod f x] x = f^[n] x
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<VAR>n : ℕ<GOAL>f^[n % Function.minimalPeriod f x] x = f^[n] x
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<VAR>hx : x ∈ Function.periodicPts f<GOAL>0 < Function.minimalPeriod f x
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<VAR>hx : x ∉ Function.periodicPts f<GOAL>Function.minimalPeriod f x = 0
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<VAR>n : ℕ<VAR>hn : 0 < n<VAR>hx : Function.IsPeriodicPt f n x<GOAL>0 < Function.minimalPeriod f x
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<GOAL>0 < Function.minimalPeriod f x ↔ x ∈ Function.periodicPts f
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<GOAL>Function.minimalPeriod f x = 0 ↔ x ∉ Function.periodicPts f
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<VAR>n : ℕ<VAR>hn : 0 < n<VAR>hx : Function.IsPeriodicPt f n x<GOAL>Function.minimalPeriod f x ≤ n
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<VAR>hx : x ∈ Function.periodicPts f<VAR>n : ℕ<GOAL>Function.minimalPeriod f (f^[n] x) = Function.minimalPeriod f x
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<VAR>hx : x ∈ Function.periodicPts f<GOAL>Function.minimalPeriod f (f x) = Function.minimalPeriod f x
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<VAR>m n : ℕ<VAR>hm : m < Function.minimalPeriod f x<VAR>hmn : f^[m] x = f^[n] x<GOAL>m ≤ n
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<GOAL>Set.InjOn (fun x_1 => f^[x_1] x) (Set.Iio (Function.minimalPeriod f x))
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<VAR>m n : ℕ<VAR>hm : m < Function.minimalPeriod f x<VAR>hn : n < Function.minimalPeriod f x<GOAL>f^[m] x = f^[n] x ↔ m = n
<VAR>α : Type u_1<VAR>x : α<GOAL>Function.minimalPeriod id x = 1
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<GOAL>Function.minimalPeriod f x = 1 ↔ Function.IsFixedPt f x
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<VAR>n : ℕ<VAR>hx : Function.IsPeriodicPt f n x<VAR>hn : n < Function.minimalPeriod f x<GOAL>n = 0
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<VAR>n : ℕ<GOAL>n ≠ 0 → n < Function.minimalPeriod f x → ¬Function.IsPeriodicPt f n x
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<VAR>n : ℕ<VAR>hx : Function.IsPeriodicPt f n x<GOAL>Function.minimalPeriod f x ∣ n
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<VAR>n : ℕ<GOAL>Function.IsPeriodicPt f n x ↔ Function.minimalPeriod f x ∣ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → α<VAR>x : α<VAR>g : β → β<VAR>y : β<GOAL>Function.minimalPeriod f x = Function.minimalPeriod g y ↔ ∀ (n : ℕ), Function.IsPeriodicPt f n x ↔ Function.IsPeriodicPt g n y
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hper : Function.IsPeriodicPt f p x<VAR>hfix : ¬Function.IsFixedPt f x<GOAL>Function.minimalPeriod f x = p
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<VAR>p k : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hk : ¬Function.IsPeriodicPt f (p ^ k) x<VAR>hk1 : Function.IsPeriodicPt f (p ^ (k + 1)) x<GOAL>Function.minimalPeriod f x = p ^ (k + 1)
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<VAR>g : α → α<VAR>h : Function.Commute f g<GOAL>Function.minimalPeriod (f ∘ g) x ∣ (Function.minimalPeriod f x).lcm (Function.minimalPeriod g x)
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<VAR>g : α → α<VAR>h : Function.Commute f g<GOAL>Function.minimalPeriod (f ∘ g) x ∣ Function.minimalPeriod f x * Function.minimalPeriod g x
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<VAR>g : α → α<VAR>h : Function.Commute f g<VAR>hco : (Function.minimalPeriod f x).Coprime (Function.minimalPeriod g x)<GOAL>Function.minimalPeriod (f ∘ g) x = Function.minimalPeriod f x * Function.minimalPeriod g x
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<VAR>n : ℕ<VAR>h : 0 < (Function.minimalPeriod f x).gcd n<GOAL>Function.minimalPeriod f^[n] x = Function.minimalPeriod f x / (Function.minimalPeriod f x).gcd n
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<VAR>n : ℕ<VAR>h : n ≠ 0<GOAL>Function.minimalPeriod f^[n] x = Function.minimalPeriod f x / (Function.minimalPeriod f x).gcd n
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<VAR>n : ℕ<VAR>h : x ∈ Function.periodicPts f<GOAL>Function.minimalPeriod f^[n] x = Function.minimalPeriod f x / (Function.minimalPeriod f x).gcd n
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<GOAL>Function.periodicOrbit f x = ↑(List.map (fun n => f^[n] x) (List.range (Function.minimalPeriod f x)))
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<GOAL>Function.periodicOrbit f x = Cycle.map (fun n => f^[n] x) ↑(List.range (Function.minimalPeriod f x))
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<GOAL>(Function.periodicOrbit f x).length = Function.minimalPeriod f x
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<GOAL>Function.periodicOrbit f x = Cycle.nil ↔ x ∉ Function.periodicPts f
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<VAR>h : x ∉ Function.periodicPts f<GOAL>Function.periodicOrbit f x = Cycle.nil
<VAR>α : Type u_1<VAR>f : α → α<VAR>x y : α<VAR>hx : x ∈ Function.periodicPts f<GOAL>y ∈ Function.periodicOrbit f x ↔ ∃ n, f^[n] x = y
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<VAR>hx : x ∈ Function.periodicPts f<VAR>n : ℕ<GOAL>f^[n] x ∈ Function.periodicOrbit f x
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<VAR>hx : x ∈ Function.periodicPts f<GOAL>x ∈ Function.periodicOrbit f x
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<GOAL>(Function.periodicOrbit f x).Nodup
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<VAR>hx : x ∈ Function.periodicPts f<VAR>n : ℕ<GOAL>Function.periodicOrbit f (f^[n] x) = Function.periodicOrbit f x
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<VAR>hx : x ∈ Function.periodicPts f<GOAL>Function.periodicOrbit f (f x) = Function.periodicOrbit f x
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>f : α → α<VAR>x : α<GOAL>Cycle.Chain r (Function.periodicOrbit f x) ↔ ∀ n < Function.minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>f : α → α<VAR>x : α<VAR>hx : x ∈ Function.periodicPts f<GOAL>Cycle.Chain r (Function.periodicOrbit f x) ↔ ∀ (n : ℕ), r (f^[n] x) (f^[n + 1] x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → α<VAR>g : β → β<VAR>x : α × β<GOAL>Function.IsFixedPt (Prod.map f g) x ↔ Function.IsFixedPt f x.1 ∧ Function.IsFixedPt g x.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → α<VAR>g : β → β<VAR>n : ℕ<VAR>x : α × β<GOAL>Function.IsPeriodicPt (Prod.map f g) n x ↔ Function.IsPeriodicPt f n x.1 ∧ Function.IsPeriodicPt g n x.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → α<VAR>g : β → β<VAR>x : α × β<GOAL>Function.minimalPeriod (Prod.map f g) x = (Function.minimalPeriod f x.1).lcm (Function.minimalPeriod g x.2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → α<VAR>g : β → β<VAR>x : α × β<GOAL>Function.minimalPeriod f x.1 ∣ Function.minimalPeriod (Prod.map f g) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → α<VAR>g : β → β<VAR>x : α × β<GOAL>Function.minimalPeriod g x.2 ∣ Function.minimalPeriod (Prod.map f g) x
<VAR>α : Type v<VAR>M : Type u<VAR>Monoid M<VAR>MulAction M α<VAR>m : M<VAR>a : α<GOAL>MulAction.period m a = Function.minimalPeriod (fun x => m • x) a
<VAR>α : Type v<VAR>M : Type u<VAR>AddMonoid M<VAR>AddAction M α<VAR>m : M<VAR>a : α<GOAL>AddAction.period m a = Function.minimalPeriod (fun x => m +ᵥ x) a
<VAR>α : Type v<VAR>M : Type u<VAR>Monoid M<VAR>MulAction M α<VAR>m : M<VAR>a : α<GOAL>m ^ MulAction.period m a • a = a
<VAR>α : Type v<VAR>M : Type u<VAR>AddMonoid M<VAR>AddAction M α<VAR>m : M<VAR>a : α<GOAL>AddAction.period m a • m +ᵥ a = a
<VAR>α : Type v<VAR>M : Type u<VAR>Monoid M<VAR>MulAction M α<VAR>m : M<VAR>a : α<VAR>n : ℕ<GOAL>Function.IsPeriodicPt (fun x => m • x) n a ↔ m ^ n • a = a
<VAR>α : Type v<VAR>M : Type u<VAR>AddMonoid M<VAR>AddAction M α<VAR>m : M<VAR>a : α<VAR>n : ℕ<GOAL>Function.IsPeriodicPt (fun x => m +ᵥ x) n a ↔ n • m +ᵥ a = a
<VAR>α : Type v<VAR>M : Type u<VAR>AddMonoid M<VAR>AddAction M α<VAR>n : ℕ<VAR>m : M<VAR>a : α<GOAL>n • m +ᵥ a = a ↔ AddAction.period m a ∣ n
<VAR>α : Type v<VAR>M : Type u<VAR>Monoid M<VAR>MulAction M α<VAR>n : ℕ<VAR>m : M<VAR>a : α<GOAL>m ^ n • a = a ↔ MulAction.period m a ∣ n
<VAR>α : Type v<VAR>G : Type u<VAR>AddGroup G<VAR>AddAction G α<VAR>j : ℤ<VAR>g : G<VAR>a : α<GOAL>j • g +ᵥ a = a ↔ ↑(AddAction.period g a) ∣ j
<VAR>α : Type v<VAR>G : Type u<VAR>Group G<VAR>MulAction G α<VAR>j : ℤ<VAR>g : G<VAR>a : α<GOAL>g ^ j • a = a ↔ ↑(MulAction.period g a) ∣ j
<VAR>α : Type v<VAR>M : Type u<VAR>AddMonoid M<VAR>AddAction M α<VAR>n : ℕ<VAR>m : M<VAR>a : α<GOAL>(n % AddAction.period m a) • m +ᵥ a = n • m +ᵥ a
<VAR>α : Type v<VAR>M : Type u<VAR>Monoid M<VAR>MulAction M α<VAR>n : ℕ<VAR>m : M<VAR>a : α<GOAL>m ^ (n % MulAction.period m a) • a = m ^ n • a
<VAR>α : Type v<VAR>G : Type u<VAR>Group G<VAR>MulAction G α<VAR>j : ℤ<VAR>g : G<VAR>a : α<GOAL>g ^ (j % ↑(MulAction.period g a)) • a = g ^ j • a
<VAR>α : Type v<VAR>G : Type u<VAR>AddGroup G<VAR>AddAction G α<VAR>j : ℤ<VAR>g : G<VAR>a : α<GOAL>(j % ↑(AddAction.period g a)) • g +ᵥ a = j • g +ᵥ a
<VAR>α : Type v<VAR>M : Type u<VAR>AddMonoid M<VAR>AddAction M α<VAR>n : ℕ<VAR>m : M<VAR>a : α<GOAL>(n + AddAction.period m a) • m +ᵥ a = n • m +ᵥ a
<VAR>α : Type v<VAR>M : Type u<VAR>Monoid M<VAR>MulAction M α<VAR>n : ℕ<VAR>m : M<VAR>a : α<GOAL>m ^ (n + MulAction.period m a) • a = m ^ n • a
<VAR>α : Type v<VAR>M : Type u<VAR>Monoid M<VAR>MulAction M α<VAR>n : ℕ<VAR>m : M<VAR>a : α<GOAL>m ^ (MulAction.period m a + n) • a = m ^ n • a
<VAR>α : Type v<VAR>M : Type u<VAR>AddMonoid M<VAR>AddAction M α<VAR>n : ℕ<VAR>m : M<VAR>a : α<GOAL>(AddAction.period m a + n) • m +ᵥ a = n • m +ᵥ a
<VAR>α : Type v<VAR>G : Type u<VAR>Group G<VAR>MulAction G α<VAR>i : ℤ<VAR>g : G<VAR>a : α<GOAL>g ^ (i + ↑(MulAction.period g a)) • a = g ^ i • a
<VAR>α : Type v<VAR>G : Type u<VAR>AddGroup G<VAR>AddAction G α<VAR>i : ℤ<VAR>g : G<VAR>a : α<GOAL>(i + ↑(AddAction.period g a)) • g +ᵥ a = i • g +ᵥ a
<VAR>α : Type v<VAR>G : Type u<VAR>AddGroup G<VAR>AddAction G α<VAR>i : ℤ<VAR>g : G<VAR>a : α<GOAL>(↑(AddAction.period g a) + i) • g +ᵥ a = i • g +ᵥ a
<VAR>α : Type v<VAR>G : Type u<VAR>Group G<VAR>MulAction G α<VAR>i : ℤ<VAR>g : G<VAR>a : α<GOAL>g ^ (↑(MulAction.period g a) + i) • a = g ^ i • a
<VAR>α : Type v<VAR>G : Type u<VAR>Group G<VAR>MulAction G α<VAR>a : G<VAR>b : α<VAR>n : ℕ<GOAL>a ^ n • b = b ↔ Function.minimalPeriod (fun x => a • x) b ∣ n
<VAR>α : Type v<VAR>G : Type u<VAR>AddGroup G<VAR>AddAction G α<VAR>a : G<VAR>b : α<VAR>n : ℕ<GOAL>n • a +ᵥ b = b ↔ Function.minimalPeriod (fun x => a +ᵥ x) b ∣ n
<VAR>α : Type v<VAR>G : Type u<VAR>Group G<VAR>MulAction G α<VAR>a : G<VAR>b : α<VAR>n : ℤ<GOAL>a ^ n • b = b ↔ ↑(Function.minimalPeriod (fun x => a • x) b) ∣ n
<VAR>α : Type v<VAR>G : Type u<VAR>AddGroup G<VAR>AddAction G α<VAR>a : G<VAR>b : α<VAR>n : ℤ<GOAL>n • a +ᵥ b = b ↔ ↑(Function.minimalPeriod (fun x => a +ᵥ x) b) ∣ n
<VAR>α : Type v<VAR>G : Type u<VAR>Group G<VAR>MulAction G α<VAR>a : G<VAR>b : α<VAR>n : ℕ<GOAL>a ^ (n % Function.minimalPeriod (fun x => a • x) b) • b = a ^ n • b
<VAR>α : Type v<VAR>G : Type u<VAR>AddGroup G<VAR>AddAction G α<VAR>a : G<VAR>b : α<VAR>n : ℕ<GOAL>(n % Function.minimalPeriod (fun x => a +ᵥ x) b) • a +ᵥ b = n • a +ᵥ b
<VAR>α : Type v<VAR>G : Type u<VAR>AddGroup G<VAR>AddAction G α<VAR>a : G<VAR>b : α<VAR>n : ℤ<GOAL>(n % ↑(Function.minimalPeriod (fun x => a +ᵥ x) b)) • a +ᵥ b = n • a +ᵥ b
<VAR>α : Type v<VAR>G : Type u<VAR>Group G<VAR>MulAction G α<VAR>a : G<VAR>b : α<VAR>n : ℤ<GOAL>a ^ (n % ↑(Function.minimalPeriod (fun x => a • x) b)) • b = a ^ n • b
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>x : E<GOAL>x ∈ separableClosure F E ↔ IsSeparable F x
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>K : Type w<VAR>Field K<VAR>Algebra F K<VAR>i : E →ₐ[F] K<VAR>x : E<GOAL>i x ∈ separableClosure F K ↔ x ∈ separableClosure F E
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>K : Type w<VAR>Field K<VAR>Algebra F K<VAR>i : E →ₐ[F] K<GOAL>IntermediateField.comap i (separableClosure F K) = separableClosure F E
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>K : Type w<VAR>Field K<VAR>Algebra F K<VAR>i : E →ₐ[F] K<GOAL>IntermediateField.map i (separableClosure F E) ≤ separableClosure F K
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>K : Type w<VAR>Field K<VAR>Algebra F K<VAR>Algebra E K<VAR>IsScalarTower F E K<VAR>h : separableClosure E K = ⊥<GOAL>IntermediateField.map (IsScalarTower.toAlgHom F E K) (separableClosure F E) = separableClosure F K
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>K : Type w<VAR>Field K<VAR>Algebra F K<VAR>i : E ≃ₐ[F] K<GOAL>IntermediateField.map (↑i) (separableClosure F E) = separableClosure F K
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>L : IntermediateField F E<VAR>hs : ∀ (x : ↥L), IsSeparable F x<GOAL>L ≤ separableClosure F E
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>L : IntermediateField F E<VAR>Algebra.IsSeparable F ↥L<GOAL>L ≤ separableClosure F E
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>L : IntermediateField F E<GOAL>L ≤ separableClosure F E ↔ Algebra.IsSeparable F ↥L
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<GOAL>separableClosure (↥(separableClosure F E)) E = ⊥
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<GOAL>normalClosure F (↥(separableClosure F E)) E = separableClosure F E
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>IsSepClosed E<GOAL>separableClosure F E = ⊥ ↔ IsSepClosed F