ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Algebra.IsIntegral K L<VAR>f g : L ≃ₐ[K] L<VAR>hfg : f ≠ g<VAR>φ : L ≃ₐ[K] L := f⁻¹ * g<VAR>x : L<VAR>hx : f x ≠ g x<VAR>hφx : φ x ≠ x<VAR>E : IntermediateField K L := K⟮x⟯<VAR>h_findim : FiniteDimensional K ↥E := IntermediateField.adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral x)<VAR>H : Subgroup (L ≃ₐ[K] L) := E.fixingSubgroup<VAR>h_basis : ↑H ∈ galGroupBasis K L<VAR>W : Set (L ≃ₐ[K] L)<VAR>hWH : W ⊆ ↑H<VAR>hW_open : IsOpen W<VAR>hW_1 : 1 ∈ W<VAR>w1 : L ≃ₐ[K] L<VAR>hw1 : w1 ∈ W<VAR>w2 : L ≃ₐ[K] L<VAR>hw2 : w2 ∈ W<VAR>h : w1 * w2⁻¹ = f⁻¹ * g<VAR>h_in_H : x ∈ E → φ x = x<VAR>hxE : x ∈ E<GOAL>False
<VAR>f✝ f g : ℝ → ℝ<VAR>hg : GrowsPolynomially g<VAR>hf : f =Θ[atTop] g<VAR>hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<GOAL>∃ c₁ > 0, ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
<VAR>f✝ f g : ℝ → ℝ<VAR>hg : GrowsPolynomially g<VAR>hf : f =Θ[atTop] g<VAR>hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<VAR>hb_pos : 0 < b<GOAL>∃ c₁ > 0, ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
<VAR>f✝ f g : ℝ → ℝ<VAR>hg : GrowsPolynomially g<VAR>hf : f =Θ[atTop] g<VAR>hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<VAR>hb_pos : 0 < b<VAR>hf_lb : ∃ c > 0, ∀ᶠ (x : ℝ) in atTop, c * ‖g x‖ ≤ ‖f x‖<GOAL>∃ c₁ > 0, ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
<VAR>f✝ f g : ℝ → ℝ<VAR>hg : GrowsPolynomially g<VAR>hf : f =Θ[atTop] g<VAR>hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<VAR>hb_pos : 0 < b<VAR>hf_lb : ∃ c > 0, ∀ᶠ (x : ℝ) in atTop, c * ‖g x‖ ≤ ‖f x‖<VAR>hf_ub : ∃ c > 0, ∀ᶠ (x : ℝ) in atTop, ‖f x‖ ≤ c * ‖g x‖<GOAL>∃ c₁ > 0, ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
<VAR>f✝ f g : ℝ → ℝ<VAR>hg : GrowsPolynomially g<VAR>hf : f =Θ[atTop] g<VAR>hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<VAR>hb_pos : 0 < b<VAR>c₁ : ℝ<VAR>hc₁_pos : 0 < c₁<VAR>hf_lb : ∀ᶠ (x : ℝ) in atTop, c₁ * ‖g x‖ ≤ ‖f x‖<VAR>c₂ : ℝ<VAR>hc₂_pos : 0 < c₂<VAR>hf_ub : ∀ᶠ (x : ℝ) in atTop, ‖f x‖ ≤ c₂ * ‖g x‖<GOAL>∃ c₁ > 0, ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
<VAR>f✝ f g : ℝ → ℝ<VAR>hg✝ : GrowsPolynomially g<VAR>hf : f =Θ[atTop] g<VAR>hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<VAR>hb_pos : 0 < b<VAR>c₁ : ℝ<VAR>hc₁_pos : 0 < c₁<VAR>hf_lb : ∀ᶠ (x : ℝ) in atTop, c₁ * ‖g x‖ ≤ ‖f x‖<VAR>c₂ : ℝ<VAR>hc₂_pos : 0 < c₂<VAR>hf_ub : ∀ᶠ (x : ℝ) in atTop, ‖f x‖ ≤ c₂ * ‖g x‖<VAR>hg : ∃ c₁ > 0, ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, (fun x => ‖g x‖) u ∈ Set.Icc (c₁ * (fun x => ‖g x‖) x) (c₂ * (fun x => ‖g x‖) x)<GOAL>∃ c₁ > 0, ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
<VAR>f✝ f g : ℝ → ℝ<VAR>hg✝ : GrowsPolynomially g<VAR>hf : f =Θ[atTop] g<VAR>hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<VAR>hb_pos : 0 < b<VAR>c₁ : ℝ<VAR>hc₁_pos : 0 < c₁<VAR>hf_lb : ∀ᶠ (x : ℝ) in atTop, c₁ * ‖g x‖ ≤ ‖f x‖<VAR>c₂ : ℝ<VAR>hc₂_pos : 0 < c₂<VAR>hf_ub : ∀ᶠ (x : ℝ) in atTop, ‖f x‖ ≤ c₂ * ‖g x‖<VAR>c₃ : ℝ<VAR>hc₃_pos : 0 < c₃<VAR>c₄ : ℝ<VAR>hc₄_pos : 0 < c₄<VAR>hg : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, (fun x => ‖g x‖) u ∈ Set.Icc (c₃ * (fun x => ‖g x‖) x) (c₄ * (fun x => ‖g x‖) x)<VAR>h_lb_pos : 0 < c₁ * c₂⁻¹ * c₃<VAR>h_ub_pos : 0 < c₂ * c₄ * c₁⁻¹<GOAL>∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * c₂⁻¹ * c₃ * f x) (c₂ * c₄ * c₁⁻¹ * f x)
<VAR>f✝ f g : ℝ → ℝ<VAR>hg✝ : GrowsPolynomially g<VAR>hf : f =Θ[atTop] g<VAR>hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<VAR>hb_pos : 0 < b<VAR>c₁ : ℝ<VAR>hc₁_pos : 0 < c₁<VAR>hf_lb : ∀ᶠ (x : ℝ) in atTop, c₁ * ‖g x‖ ≤ ‖f x‖<VAR>c₂ : ℝ<VAR>hc₂_pos : 0 < c₂<VAR>hf_ub : ∀ᶠ (x : ℝ) in atTop, ‖f x‖ ≤ c₂ * ‖g x‖<VAR>c₃ : ℝ<VAR>hc₃_pos : 0 < c₃<VAR>c₄ : ℝ<VAR>hc₄_pos : 0 < c₄<VAR>hg : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, (fun x => ‖g x‖) u ∈ Set.Icc (c₃ * (fun x => ‖g x‖) x) (c₄ * (fun x => ‖g x‖) x)<VAR>h_lb_pos : 0 < c₁ * c₂⁻¹ * c₃<VAR>h_ub_pos : 0 < c₂ * c₄ * c₁⁻¹<VAR>c₂_cancel : c₂⁻¹ * c₂ = 1<GOAL>∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * c₂⁻¹ * c₃ * f x) (c₂ * c₄ * c₁⁻¹ * f x)
<VAR>f✝ f g : ℝ → ℝ<VAR>hg✝ : GrowsPolynomially g<VAR>hf : f =Θ[atTop] g<VAR>hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<VAR>hb_pos : 0 < b<VAR>c₁ : ℝ<VAR>hc₁_pos : 0 < c₁<VAR>hf_lb : ∀ᶠ (x : ℝ) in atTop, c₁ * ‖g x‖ ≤ ‖f x‖<VAR>c₂ : ℝ<VAR>hc₂_pos : 0 < c₂<VAR>hf_ub : ∀ᶠ (x : ℝ) in atTop, ‖f x‖ ≤ c₂ * ‖g x‖<VAR>c₃ : ℝ<VAR>hc₃_pos : 0 < c₃<VAR>c₄ : ℝ<VAR>hc₄_pos : 0 < c₄<VAR>hg : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, (fun x => ‖g x‖) u ∈ Set.Icc (c₃ * (fun x => ‖g x‖) x) (c₄ * (fun x => ‖g x‖) x)<VAR>h_lb_pos : 0 < c₁ * c₂⁻¹ * c₃<VAR>h_ub_pos : 0 < c₂ * c₄ * c₁⁻¹<VAR>c₂_cancel : c₂⁻¹ * c₂ = 1<VAR>c₁_cancel : c₁⁻¹ * c₁ = 1<GOAL>∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * c₂⁻¹ * c₃ * f x) (c₂ * c₄ * c₁⁻¹ * f x)
<VAR>f✝ f g : ℝ → ℝ<VAR>hg✝ : GrowsPolynomially g<VAR>hf : f =Θ[atTop] g<VAR>hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<VAR>hb_pos : 0 < b<VAR>c₁ : ℝ<VAR>hc₁_pos : 0 < c₁<VAR>hf_lb : ∀ᶠ (x : ℝ) in atTop, c₁ * ‖g x‖ ≤ ‖f x‖<VAR>c₂ : ℝ<VAR>hc₂_pos : 0 < c₂<VAR>hf_ub : ∀ᶠ (x : ℝ) in atTop, ‖f x‖ ≤ c₂ * ‖g x‖<VAR>c₃ : ℝ<VAR>hc₃_pos : 0 < c₃<VAR>c₄ : ℝ<VAR>hc₄_pos : 0 < c₄<VAR>hg : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, (fun x => ‖g x‖) u ∈ Set.Icc (c₃ * (fun x => ‖g x‖) x) (c₄ * (fun x => ‖g x‖) x)<VAR>h_lb_pos : 0 < c₁ * c₂⁻¹ * c₃<VAR>h_ub_pos : 0 < c₂ * c₄ * c₁⁻¹<VAR>c₂_cancel : c₂⁻¹ * c₂ = 1<VAR>c₁_cancel : c₁⁻¹ * c₁ = 1<VAR>x : ℝ<VAR>hf_pos : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y<VAR>h_lb : ∀ (y : ℝ), b * id x ≤ y → c₁ * ‖g y‖ ≤ ‖f y‖<VAR>h_ub : ∀ (y : ℝ), b * id x ≤ y → ‖f y‖ ≤ c₂ * ‖g y‖<VAR>hg_bound : ∀ (y : ℝ), b * id x ≤ y → ∀ u ∈ Set.Icc (b * y) y, ‖g u‖ ∈ Set.Icc (c₃ * ‖g y‖) (c₄ * ‖g y‖)<VAR>hx_pos : 0 ≤ x<GOAL>∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * c₂⁻¹ * c₃ * f x) (c₂ * c₄ * c₁⁻¹ * f x)
<VAR>f✝ f g : ℝ → ℝ<VAR>hg✝ : GrowsPolynomially g<VAR>hf : f =Θ[atTop] g<VAR>hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<VAR>hb_pos : 0 < b<VAR>c₁ : ℝ<VAR>hc₁_pos : 0 < c₁<VAR>hf_lb : ∀ᶠ (x : ℝ) in atTop, c₁ * ‖g x‖ ≤ ‖f x‖<VAR>c₂ : ℝ<VAR>hc₂_pos : 0 < c₂<VAR>hf_ub : ∀ᶠ (x : ℝ) in atTop, ‖f x‖ ≤ c₂ * ‖g x‖<VAR>c₃ : ℝ<VAR>hc₃_pos : 0 < c₃<VAR>c₄ : ℝ<VAR>hc₄_pos : 0 < c₄<VAR>hg : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, (fun x => ‖g x‖) u ∈ Set.Icc (c₃ * (fun x => ‖g x‖) x) (c₄ * (fun x => ‖g x‖) x)<VAR>h_lb_pos : 0 < c₁ * c₂⁻¹ * c₃<VAR>h_ub_pos : 0 < c₂ * c₄ * c₁⁻¹<VAR>c₂_cancel : c₂⁻¹ * c₂ = 1<VAR>c₁_cancel : c₁⁻¹ * c₁ = 1<VAR>x : ℝ<VAR>hf_pos : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y<VAR>h_lb : ∀ (y : ℝ), b * id x ≤ y → c₁ * ‖g y‖ ≤ ‖f y‖<VAR>h_ub : ∀ (y : ℝ), b * id x ≤ y → ‖f y‖ ≤ c₂ * ‖g y‖<VAR>hg_bound : ∀ (y : ℝ), b * id x ≤ y → ∀ u ∈ Set.Icc (b * y) y, ‖g u‖ ∈ Set.Icc (c₃ * ‖g y‖) (c₄ * ‖g y‖)<VAR>hx_pos : 0 ≤ x<VAR>u : ℝ<VAR>hu : u ∈ Set.Icc (b * x) x<GOAL>f u ∈ Set.Icc (c₁ * c₂⁻¹ * c₃ * f x) (c₂ * c₄ * c₁⁻¹ * f x)
<VAR>f✝ f g : ℝ → ℝ<VAR>hg✝ : GrowsPolynomially g<VAR>hf : f =Θ[atTop] g<VAR>hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<VAR>hb_pos : 0 < b<VAR>c₁ : ℝ<VAR>hc₁_pos : 0 < c₁<VAR>hf_lb : ∀ᶠ (x : ℝ) in atTop, c₁ * ‖g x‖ ≤ ‖f x‖<VAR>c₂ : ℝ<VAR>hc₂_pos : 0 < c₂<VAR>hf_ub : ∀ᶠ (x : ℝ) in atTop, ‖f x‖ ≤ c₂ * ‖g x‖<VAR>c₃ : ℝ<VAR>hc₃_pos : 0 < c₃<VAR>c₄ : ℝ<VAR>hc₄_pos : 0 < c₄<VAR>hg : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, (fun x => ‖g x‖) u ∈ Set.Icc (c₃ * (fun x => ‖g x‖) x) (c₄ * (fun x => ‖g x‖) x)<VAR>h_lb_pos : 0 < c₁ * c₂⁻¹ * c₃<VAR>h_ub_pos : 0 < c₂ * c₄ * c₁⁻¹<VAR>c₂_cancel : c₂⁻¹ * c₂ = 1<VAR>c₁_cancel : c₁⁻¹ * c₁ = 1<VAR>x : ℝ<VAR>hf_pos : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y<VAR>h_lb : ∀ (y : ℝ), b * id x ≤ y → c₁ * ‖g y‖ ≤ ‖f y‖<VAR>h_ub : ∀ (y : ℝ), b * id x ≤ y → ‖f y‖ ≤ c₂ * ‖g y‖<VAR>hg_bound : ∀ (y : ℝ), b * id x ≤ y → ∀ u ∈ Set.Icc (b * y) y, ‖g u‖ ∈ Set.Icc (c₃ * ‖g y‖) (c₄ * ‖g y‖)<VAR>hx_pos : 0 ≤ x<VAR>u : ℝ<VAR>hu : u ∈ Set.Icc (b * x) x<VAR>hbx : b * x ≤ x<GOAL>f u ∈ Set.Icc (c₁ * c₂⁻¹ * c₃ * f x) (c₂ * c₄ * c₁⁻¹ * f x)
<VAR>f✝ f g : ℝ → ℝ<VAR>hg✝ : GrowsPolynomially g<VAR>hf : f =Θ[atTop] g<VAR>hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<VAR>hb_pos : 0 < b<VAR>c₁ : ℝ<VAR>hc₁_pos : 0 < c₁<VAR>hf_lb : ∀ᶠ (x : ℝ) in atTop, c₁ * ‖g x‖ ≤ ‖f x‖<VAR>c₂ : ℝ<VAR>hc₂_pos : 0 < c₂<VAR>hf_ub : ∀ᶠ (x : ℝ) in atTop, ‖f x‖ ≤ c₂ * ‖g x‖<VAR>c₃ : ℝ<VAR>hc₃_pos : 0 < c₃<VAR>c₄ : ℝ<VAR>hc₄_pos : 0 < c₄<VAR>hg : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, (fun x => ‖g x‖) u ∈ Set.Icc (c₃ * (fun x => ‖g x‖) x) (c₄ * (fun x => ‖g x‖) x)<VAR>h_lb_pos : 0 < c₁ * c₂⁻¹ * c₃<VAR>h_ub_pos : 0 < c₂ * c₄ * c₁⁻¹<VAR>c₂_cancel : c₂⁻¹ * c₂ = 1<VAR>c₁_cancel : c₁⁻¹ * c₁ = 1<VAR>x : ℝ<VAR>hf_pos : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y<VAR>h_lb : ∀ (y : ℝ), b * id x ≤ y → c₁ * ‖g y‖ ≤ ‖f y‖<VAR>h_ub : ∀ (y : ℝ), b * id x ≤ y → ‖f y‖ ≤ c₂ * ‖g y‖<VAR>hg_bound✝ : ∀ (y : ℝ), b * id x ≤ y → ∀ u ∈ Set.Icc (b * y) y, ‖g u‖ ∈ Set.Icc (c₃ * ‖g y‖) (c₄ * ‖g y‖)<VAR>hx_pos : 0 ≤ x<VAR>u : ℝ<VAR>hu : u ∈ Set.Icc (b * x) x<VAR>hbx : b * x ≤ x<VAR>hg_bound : ∀ u ∈ Set.Icc (b * x) x, ‖g u‖ ∈ Set.Icc (c₃ * ‖g x‖) (c₄ * ‖g x‖)<GOAL>c₁ * c₂⁻¹ * c₃ * f x ≤ f u
<VAR>f✝ f g : ℝ → ℝ<VAR>hg✝ : GrowsPolynomially g<VAR>hf : f =Θ[atTop] g<VAR>hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<VAR>hb_pos : 0 < b<VAR>c₁ : ℝ<VAR>hc₁_pos : 0 < c₁<VAR>hf_lb : ∀ᶠ (x : ℝ) in atTop, c₁ * ‖g x‖ ≤ ‖f x‖<VAR>c₂ : ℝ<VAR>hc₂_pos : 0 < c₂<VAR>hf_ub : ∀ᶠ (x : ℝ) in atTop, ‖f x‖ ≤ c₂ * ‖g x‖<VAR>c₃ : ℝ<VAR>hc₃_pos : 0 < c₃<VAR>c₄ : ℝ<VAR>hc₄_pos : 0 < c₄<VAR>hg : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, (fun x => ‖g x‖) u ∈ Set.Icc (c₃ * (fun x => ‖g x‖) x) (c₄ * (fun x => ‖g x‖) x)<VAR>h_lb_pos : 0 < c₁ * c₂⁻¹ * c₃<VAR>h_ub_pos : 0 < c₂ * c₄ * c₁⁻¹<VAR>c₂_cancel : c₂⁻¹ * c₂ = 1<VAR>c₁_cancel : c₁⁻¹ * c₁ = 1<VAR>x : ℝ<VAR>hf_pos : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y<VAR>h_lb : ∀ (y : ℝ), b * id x ≤ y → c₁ * ‖g y‖ ≤ ‖f y‖<VAR>h_ub : ∀ (y : ℝ), b * id x ≤ y → ‖f y‖ ≤ c₂ * ‖g y‖<VAR>hg_bound✝ : ∀ (y : ℝ), b * id x ≤ y → ∀ u ∈ Set.Icc (b * y) y, ‖g u‖ ∈ Set.Icc (c₃ * ‖g y‖) (c₄ * ‖g y‖)<VAR>hx_pos : 0 ≤ x<VAR>u : ℝ<VAR>hu : u ∈ Set.Icc (b * x) x<VAR>hbx : b * x ≤ x<VAR>hg_bound : ∀ u ∈ Set.Icc (b * x) x, ‖g u‖ ∈ Set.Icc (c₃ * ‖g x‖) (c₄ * ‖g x‖)<GOAL>f u ≤ c₂ * c₄ * c₁⁻¹ * f x
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>s : Set (Filter α)<VAR>l : Filter α<GOAL>l ∈ interior s ↔ ∃ t ∈ l, Iic (𝓟 t) ⊆ s
<VAR>F : Type u<VAR>K : Type v<VAR>A : Type w<VAR>inst✝¹⁰ : Ring F<VAR>inst✝⁹ : Ring K<VAR>inst✝⁸ : AddCommGroup A<VAR>inst✝⁷ : Module F K<VAR>inst✝⁶ : Module K A<VAR>inst✝⁵ : Module F A<VAR>inst✝⁴ : IsScalarTower F K A<VAR>inst✝³ : StrongRankCondition F<VAR>inst✝² : StrongRankCondition K<VAR>inst✝¹ : Module.Free F K<VAR>inst✝ : Module.Free K A<GOAL>toNat (Module.rank F K) * toNat (Module.rank K A) = toNat (Module.rank F A)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝² : Category.{v', u'} D<VAR>inst✝¹ : HasZeroObject C<VAR>inst✝ : HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>i : Y ≅ 0<VAR>Z : C<VAR>g h : Y ⟶ Z<VAR>x✝ : f ≫ g = f ≫ h<GOAL>g = h
<VAR>m n : ℕ<GOAL>m < 2 ^ n → m.size ≤ n
<VAR>m n : ℕ<GOAL>m < 1 <<< n → m.size ≤ n
<VAR>A : Type u_1<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : StarRing A<VAR>inst✝² : TopologicalSpace A<VAR>inst✝¹ : Algebra ℝ A<VAR>inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint<VAR>a : A<VAR>ha₁ : IsSelfAdjoint a<VAR>ha₂ : SpectrumRestricts a ⇑ContinuousMap.realToNNReal<GOAL>∃ x, IsSelfAdjoint x ∧ SpectrumRestricts x ⇑ContinuousMap.realToNNReal ∧ x ^ 2 = a
<VAR>A : Type u_1<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : StarRing A<VAR>inst✝² : TopologicalSpace A<VAR>inst✝¹ : Algebra ℝ A<VAR>inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint<VAR>a : A<VAR>ha₁ : IsSelfAdjoint a<VAR>ha₂ : SpectrumRestricts a ⇑ContinuousMap.realToNNReal<GOAL>SpectrumRestricts (cfc Real.sqrt a) ⇑ContinuousMap.realToNNReal ∧ cfc Real.sqrt a ^ 2 = a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : CommRing T<VAR>inst✝¹² : Algebra R S<VAR>inst✝¹¹ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Field L<VAR>inst✝⁸ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝⁷ : Fintype ι<VAR>F : Type u_6<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Algebra R L<VAR>inst✝⁴ : Algebra L F<VAR>inst✝³ : Algebra R F<VAR>inst✝² : IsScalarTower R L F<VAR>pb : PowerBasis K L<VAR>inst✝¹ : Algebra.IsSeparable K L<VAR>inst✝ : DecidableEq ι<VAR>b : Basis ι K L<GOAL>((BilinForm.toMatrix b) (traceForm K L)).det ≠ 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : CommRing T<VAR>inst✝¹² : Algebra R S<VAR>inst✝¹¹ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Field L<VAR>inst✝⁸ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝⁷ : Fintype ι<VAR>F : Type u_6<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Algebra R L<VAR>inst✝⁴ : Algebra L F<VAR>inst✝³ : Algebra R F<VAR>inst✝² : IsScalarTower R L F<VAR>pb : PowerBasis K L<VAR>inst✝¹ : Algebra.IsSeparable K L<VAR>inst✝ : DecidableEq ι<VAR>b : Basis ι K L<VAR>this : FiniteDimensional K L<GOAL>((BilinForm.toMatrix b) (traceForm K L)).det ≠ 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : CommRing T<VAR>inst✝¹² : Algebra R S<VAR>inst✝¹¹ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Field L<VAR>inst✝⁸ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝⁷ : Fintype ι<VAR>F : Type u_6<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Algebra R L<VAR>inst✝⁴ : Algebra L F<VAR>inst✝³ : Algebra R F<VAR>inst✝² : IsScalarTower R L F<VAR>pb✝ : PowerBasis K L<VAR>inst✝¹ : Algebra.IsSeparable K L<VAR>inst✝ : DecidableEq ι<VAR>b : Basis ι K L<VAR>this : FiniteDimensional K L<VAR>pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L<GOAL>((BilinForm.toMatrix b) (traceForm K L)).det ≠ 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : CommRing T<VAR>inst✝¹² : Algebra R S<VAR>inst✝¹¹ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Field L<VAR>inst✝⁸ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝⁷ : Fintype ι<VAR>F : Type u_6<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Algebra R L<VAR>inst✝⁴ : Algebra L F<VAR>inst✝³ : Algebra R F<VAR>inst✝² : IsScalarTower R L F<VAR>pb✝ : PowerBasis K L<VAR>inst✝¹ : Algebra.IsSeparable K L<VAR>inst✝ : DecidableEq ι<VAR>b : Basis ι K L<VAR>this : FiniteDimensional K L<VAR>pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L<GOAL>(pb.basis.toMatrix ⇑b * (pb.basis.toMatrix ⇑b)ᵀ).det * ((BilinForm.toMatrix pb.basis) (traceForm K L)).det ≠ 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : CommRing T<VAR>inst✝¹² : Algebra R S<VAR>inst✝¹¹ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Field L<VAR>inst✝⁸ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝⁷ : Fintype ι<VAR>F : Type u_6<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Algebra R L<VAR>inst✝⁴ : Algebra L F<VAR>inst✝³ : Algebra R F<VAR>inst✝² : IsScalarTower R L F<VAR>pb✝ : PowerBasis K L<VAR>inst✝¹ : Algebra.IsSeparable K L<VAR>inst✝ : DecidableEq ι<VAR>b : Basis ι K L<VAR>this : FiniteDimensional K L<VAR>pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L<GOAL>b.toMatrix ⇑pb.basis * pb.basis.toMatrix ⇑b = 1
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : CommRing T<VAR>inst✝¹² : Algebra R S<VAR>inst✝¹¹ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Field L<VAR>inst✝⁸ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝⁷ : Fintype ι<VAR>F : Type u_6<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Algebra R L<VAR>inst✝⁴ : Algebra L F<VAR>inst✝³ : Algebra R F<VAR>inst✝² : IsScalarTower R L F<VAR>pb✝ : PowerBasis K L<VAR>inst✝¹ : Algebra.IsSeparable K L<VAR>inst✝ : DecidableEq ι<VAR>b : Basis ι K L<VAR>this : FiniteDimensional K L<VAR>pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L<GOAL>(pb.basis.toMatrix ⇑b * (pb.basis.toMatrix ⇑b)ᵀ).det * ((b.toMatrix ⇑pb.basis)ᵀ * b.toMatrix ⇑pb.basis).det = 1
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : CommRing T<VAR>inst✝¹² : Algebra R S<VAR>inst✝¹¹ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Field L<VAR>inst✝⁸ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝⁷ : Fintype ι<VAR>F : Type u_6<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Algebra R L<VAR>inst✝⁴ : Algebra L F<VAR>inst✝³ : Algebra R F<VAR>inst✝² : IsScalarTower R L F<VAR>pb✝ : PowerBasis K L<VAR>inst✝¹ : Algebra.IsSeparable K L<VAR>inst✝ : DecidableEq ι<VAR>b : Basis ι K L<VAR>this : FiniteDimensional K L<VAR>pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L<GOAL>((BilinForm.toMatrix pb.basis) (traceForm K L)).det ≠ 0
<VAR>R : Type u_1<VAR>inst✝¹² : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝¹¹ : CommRing S<VAR>inst✝¹⁰ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁹ : CommRing P<VAR>Rₘ : Type u_4<VAR>Sₘ : Type u_5<VAR>inst✝⁸ : CommRing Rₘ<VAR>inst✝⁷ : CommRing Sₘ<VAR>inst✝⁶ : Algebra R Rₘ<VAR>inst✝⁵ : IsLocalization M Rₘ<VAR>inst✝⁴ : Algebra S Sₘ<VAR>i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ<VAR>inst✝³ : Algebra Rₘ Sₘ<VAR>inst✝² : Algebra R Sₘ<VAR>inst✝¹ : IsScalarTower R Rₘ Sₘ<VAR>inst✝ : IsScalarTower R S Sₘ<VAR>x : R<VAR>y : ↥M<GOAL>(algebraMap Rₘ Sₘ) (mk' Rₘ x y) = mk' Sₘ ((algebraMap R S) x) ⟨(algebraMap R S) ↑y, ⋯⟩
<VAR>R : Type u_1<VAR>inst✝¹² : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝¹¹ : CommRing S<VAR>inst✝¹⁰ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁹ : CommRing P<VAR>Rₘ : Type u_4<VAR>Sₘ : Type u_5<VAR>inst✝⁸ : CommRing Rₘ<VAR>inst✝⁷ : CommRing Sₘ<VAR>inst✝⁶ : Algebra R Rₘ<VAR>inst✝⁵ : IsLocalization M Rₘ<VAR>inst✝⁴ : Algebra S Sₘ<VAR>i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ<VAR>inst✝³ : Algebra Rₘ Sₘ<VAR>inst✝² : Algebra R Sₘ<VAR>inst✝¹ : IsScalarTower R Rₘ Sₘ<VAR>inst✝ : IsScalarTower R S Sₘ<VAR>x : R<VAR>y : ↥M<GOAL>(algebraMap Rₘ Sₘ) (mk' Rₘ (↑y * x) y) = (algebraMap Rₘ Sₘ) ((algebraMap R Rₘ) x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>t : Set α<VAR>i : ι<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>i' : ι'<VAR>hl : l.HasBasis p s<VAR>h : ∀ (i : ι), p i → ∃ i', p' i' ∧ s' i' ⊆ s i<VAR>h' : ∀ (i' : ι'), p' i' → s' i' ∈ l<GOAL>l.HasBasis p' s'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>t✝ : Set α<VAR>i : ι<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>i' : ι'<VAR>hl : l.HasBasis p s<VAR>h : ∀ (i : ι), p i → ∃ i', p' i' ∧ s' i' ⊆ s i<VAR>h' : ∀ (i' : ι'), p' i' → s' i' ∈ l<VAR>t : Set α<VAR>ht : t ∈ l<GOAL>∃ i, p' i ∧ s' i ⊆ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>t✝ : Set α<VAR>i✝ : ι<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>i' : ι'<VAR>hl : l.HasBasis p s<VAR>h : ∀ (i : ι), p i → ∃ i', p' i' ∧ s' i' ⊆ s i<VAR>h' : ∀ (i' : ι'), p' i' → s' i' ∈ l<VAR>t : Set α<VAR>ht✝ : t ∈ l<VAR>i : ι<VAR>hi : p i<VAR>ht : s i ⊆ t<GOAL>∃ i, p' i ∧ s' i ⊆ t
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>n : ℤ<GOAL>↑(T ^ n • z) = ↑z + ↑n
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>n : ℤ<GOAL>num (↑(T ^ n)) z / denom (↑(T ^ n)) z = ↑z + ↑n
<VAR>C : Type u₁<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>inst✝³ : HasZeroMorphisms D<VAR>F : C ⥤ D<VAR>inst✝² : F.PreservesZeroMorphisms<VAR>J : Type w₁<VAR>f : J → C<VAR>inst✝¹ : HasBiproduct f<VAR>inst✝ : PreservesBiproduct f F<VAR>W : C<VAR>g : (j : J) → W ⟶ f j<VAR>j : J<GOAL>(F.map (lift g) ≫ (F.mapBiproduct f).hom) ≫ π (F.obj ∘ f) j = (lift fun j => F.map (g j)) ≫ π (F.obj ∘ f) j
<VAR>C : Type u₁<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>inst✝³ : HasZeroMorphisms D<VAR>F : C ⥤ D<VAR>inst✝² : F.PreservesZeroMorphisms<VAR>J : Type w₁<VAR>f : J → C<VAR>inst✝¹ : HasBiproduct f<VAR>inst✝ : PreservesBiproduct f F<VAR>W : C<VAR>g : (j : J) → W ⟶ f j<VAR>j : J<GOAL>(F.map (lift g) ≫ (F.mapBiproduct f).hom) ≫ π (fun x => F.obj (f x)) j = (lift fun j => F.map (g j)) ≫ π (fun x => F.obj (f x)) j
<VAR>C : Type u₁<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>inst✝³ : HasZeroMorphisms D<VAR>F : C ⥤ D<VAR>inst✝² : F.PreservesZeroMorphisms<VAR>J : Type w₁<VAR>f : J → C<VAR>inst✝¹ : HasBiproduct f<VAR>inst✝ : PreservesBiproduct f F<VAR>W : C<VAR>g : (j : J) → W ⟶ f j<VAR>j : J<VAR>this : HasBiproduct fun j => F.obj (f j)<GOAL>(F.map (lift g) ≫ (F.mapBiproduct f).hom) ≫ π (fun x => F.obj (f x)) j = (lift fun j => F.map (g j)) ≫ π (fun x => F.obj (f x)) j
<VAR>m n : ℕ+<GOAL>m ∣ n ↔ n.gcd m = m
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype β<VAR>f : α ≃ β<GOAL>card α = card β
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype β<VAR>f : α ≃ β<GOAL>card β = card β
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>P : Cᵒᵖ ⥤ Type (max v u)<VAR>X : C<VAR>R : Presieve X<VAR>S : Sieve X<VAR>z₁ z₂ : FirstObj P R<VAR>h : ∀ (Y : C) (f : Y ⟶ X) (hf : R f), Pi.π (fun f => P.obj (op f.fst)) ⟨Y, ⟨f, hf⟩⟩ z₁ = Pi.π (fun f => P.obj (op f.fst)) ⟨Y, ⟨f, hf⟩⟩ z₂<GOAL>z₁ = z₂
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>P : Cᵒᵖ ⥤ Type (max v u)<VAR>X : C<VAR>R : Presieve X<VAR>S : Sieve X<VAR>z₁ z₂ : FirstObj P R<VAR>h : ∀ (Y : C) (f : Y ⟶ X) (hf : R f), Pi.π (fun f => P.obj (op f.fst)) ⟨Y, ⟨f, hf⟩⟩ z₁ = Pi.π (fun f => P.obj (op f.fst)) ⟨Y, ⟨f, hf⟩⟩ z₂<GOAL>∀ (j : Discrete ((Y : C) × { f // R f })), limit.π (Discrete.functor fun f => P.obj (op f.fst)) j z₁ = limit.π (Discrete.functor fun f => P.obj (op f.fst)) j z₂
<VAR>α : Type u_1<VAR>inst✝ : AddCommGroup α<VAR>n : ℤ<VAR>x a : α<VAR>n' : ℤ<VAR>a' : α<VAR>h₁ : -n = n'<VAR>h₂ : -a = a'<GOAL>-termg n x a = termg n' x a'
<VAR>α : Type u_1<VAR>inst✝ : Group α<VAR>s : Subgroup α<VAR>a : α<VAR>ha : a ∈ s<GOAL>∀ (x : α), x ∈ a • ↑s ↔ x ∈ ↑s
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n p✝ : R<VAR>k✝ : ℕ<VAR>x✝ : ∃ p k, Prime p ∧ 0 < k ∧ p ^ k = n<VAR>p : R<VAR>k : ℕ<VAR>hp : Prime p<VAR>hk : 0 < k<VAR>hn : p ^ k = n<GOAL>p ^ (k - 1 + 1) = n
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>S : Type v<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>p : S[X]<GOAL>p ∈ lifts f ↔ p ∈ Set.range (map f)
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>n : ℕ<VAR>hζ : (primitiveRoots n K).Nonempty<VAR>hn : 0 < n<VAR>a : K<VAR>H : Irreducible (X ^ n - C a)<VAR>this✝ : Fact (Irreducible (X ^ n - C a)) := { out := H }<VAR>this : Algebra K K[n√a] := inferInstance<GOAL>(X ^ n - C a).Separable
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>n : ℕ<VAR>hζ : (primitiveRoots n K).Nonempty<VAR>hn✝ : 0 < n<VAR>a : K<VAR>H : Irreducible (X ^ n - C a)<VAR>this✝ : Fact (Irreducible (X ^ n - C a)) := { out := H }<VAR>this : Algebra K K[n√a] := inferInstance<VAR>hn : 0 < n<GOAL>(X ^ n - C a).Separable
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>n : ℕ<VAR>hζ✝ : (primitiveRoots n K).Nonempty<VAR>hn✝ : 0 < n<VAR>a : K<VAR>H : Irreducible (X ^ n - C a)<VAR>this✝ : Fact (Irreducible (X ^ n - C a)) := { out := H }<VAR>this : Algebra K K[n√a] := inferInstance<VAR>hn : 0 < n<VAR>hn' : ¬n = 1<VAR>ζ : K<VAR>hζ : ζ ∈ primitiveRoots n K<GOAL>(X ^ n - C a).Separable