ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>S : Set E<GOAL>Algebra.IsSeparable F ↥(IntermediateField.adjoin F S) ↔ ∀ x ∈ S, IsSeparable F x
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<GOAL>separableClosure F E = ⊤ ↔ Algebra.IsSeparable 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>Algebra E K<VAR>IsScalarTower F E K<GOAL>separableClosure F K ≤ IntermediateField.restrictScalars F (separableClosure E 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>Algebra.IsSeparable F E<GOAL>separableClosure F K = IntermediateField.restrictScalars F (separableClosure E 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<GOAL>IntermediateField.adjoin E ↑(separableClosure F K) ≤ separableClosure E K
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<GOAL>Field.finInsepDegree F E = Cardinal.toNat (Field.insepDegree 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>Cardinal.lift.{w, v} (Field.sepDegree F E) = Cardinal.lift.{v, w} (Field.sepDegree F K)
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>K : Type v<VAR>Field K<VAR>Algebra F K<VAR>i : E ≃ₐ[F] K<GOAL>Field.sepDegree F E = Field.sepDegree F K
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<GOAL>Field.sepDegree F E * Field.insepDegree F E = Module.rank 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>Cardinal.lift.{w, v} (Field.insepDegree F E) = Cardinal.lift.{v, w} (Field.insepDegree F K)
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>K : Type v<VAR>Field K<VAR>Algebra F K<VAR>i : E ≃ₐ[F] K<GOAL>Field.insepDegree F E = Field.insepDegree 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>Field.finInsepDegree F E = Field.finInsepDegree F K
<VAR>F : Type u<VAR>Field F<GOAL>Field.sepDegree F F = 1
<VAR>F : Type u<VAR>Field F<GOAL>Field.insepDegree F F = 1
<VAR>F : Type u<VAR>Field F<GOAL>Field.finInsepDegree F F = 1
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<GOAL>Field.sepDegree F ↥⊥ = 1
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<GOAL>Field.insepDegree F ↥⊥ = 1
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<GOAL>Field.finInsepDegree F ↥⊥ = 1
<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<GOAL>Cardinal.lift.{v, w} (Field.sepDegree F ↥⊥) = Cardinal.lift.{w, v} (Field.sepDegree 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>Algebra E K<VAR>IsScalarTower F E K<GOAL>Cardinal.lift.{v, w} (Field.insepDegree F ↥⊥) = Cardinal.lift.{w, v} (Field.insepDegree 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>Algebra E K<VAR>IsScalarTower F E K<GOAL>Field.finInsepDegree F ↥⊥ = Field.finInsepDegree 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>Algebra E K<VAR>IsScalarTower F E K<GOAL>Field.sepDegree F ↥⊤ = Field.sepDegree 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<GOAL>Field.insepDegree F ↥⊤ = Field.insepDegree 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<GOAL>Field.finInsepDegree F ↥⊤ = Field.finInsepDegree F K
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>K : Type v<VAR>Field K<VAR>Algebra F K<VAR>Algebra E K<VAR>IsScalarTower F E K<GOAL>Field.sepDegree F ↥⊥ = Field.sepDegree F E
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>K : Type v<VAR>Field K<VAR>Algebra F K<VAR>Algebra E K<VAR>IsScalarTower F E K<GOAL>Field.insepDegree F ↥⊥ = Field.insepDegree F E
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>Algebra.IsSeparable F E<GOAL>Field.sepDegree F E = Module.rank F E
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>Algebra.IsSeparable F E<GOAL>Field.insepDegree F E = 1
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>Algebra.IsSeparable F E<GOAL>Field.finInsepDegree F E = 1
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>self : IsGalois F E<GOAL>Normal F E
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>self : IsGalois F E<GOAL>Algebra.IsSeparable F E
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<GOAL>IsGalois F E ↔ Algebra.IsSeparable F E ∧ Normal F E
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>IsGalois F E<VAR>x : E<GOAL>IsIntegral F x
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>IsGalois F E<VAR>x : E<GOAL>IsSeparable F x
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>IsGalois F E<VAR>x : E<GOAL>Polynomial.Splits (algebraMap F E) (minpoly F x)
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>FiniteDimensional F E<VAR>α : E<VAR>hα : IsIntegral F α<VAR>h_sep : IsSeparable F α<VAR>h_splits : Polynomial.Splits (algebraMap F ↥F⟮α⟯) (minpoly F α)<GOAL>Fintype.card (↥F⟮α⟯ ≃ₐ[F] ↥F⟮α⟯) = FiniteDimensional.finrank F ↥F⟮α⟯
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>FiniteDimensional F E<VAR>IsGalois F E<GOAL>Fintype.card (E ≃ₐ[F] E) = FiniteDimensional.finrank F E
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>E : Type u_3<VAR>Field F<VAR>Field K<VAR>Field E<VAR>Algebra F K<VAR>Algebra F E<VAR>Algebra K E<VAR>IsScalarTower F K E<VAR>IsGalois F E<GOAL>IsGalois K E
<VAR>F : Type u_1<VAR>E : Type u_3<VAR>Field F<VAR>Field E<VAR>Algebra F E<GOAL>IsGalois (↥⊥) E ↔ IsGalois F E
<VAR>F : Type u_1<VAR>E : Type u_3<VAR>Field F<VAR>Field E<VAR>E' : Type u_4<VAR>Field E'<VAR>Algebra F E'<VAR>Algebra F E<VAR>IsGalois F E<VAR>f : E ≃ₐ[F] E'<GOAL>IsGalois F E'
<VAR>F : Type u_1<VAR>E : Type u_3<VAR>Field F<VAR>Field E<VAR>E' : Type u_4<VAR>Field E'<VAR>Algebra F E'<VAR>Algebra F E<VAR>f : E ≃ₐ[F] E'<GOAL>IsGalois F E ↔ IsGalois F E'
<VAR>F : Type u_1<VAR>E : Type u_3<VAR>Field F<VAR>Field E<VAR>Algebra F E<GOAL>IsGalois F ↥⊤ ↔ IsGalois F E
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>H : Subgroup (E ≃ₐ[F] E)<VAR>FiniteDimensional F E<VAR>DecidablePred fun x => x ∈ H<GOAL>FiniteDimensional.finrank (↥(IntermediateField.fixedField H)) E = Fintype.card ↥H
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>H : Subgroup (E ≃ₐ[F] E)<VAR>K : IntermediateField F E<GOAL>K ≤ IntermediateField.fixedField H ↔ H ≤ K.fixingSubgroup
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>H : Subgroup (E ≃ₐ[F] E)<VAR>FiniteDimensional F E<GOAL>(IntermediateField.fixedField H).fixingSubgroup = H
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>K : IntermediateField F E<VAR>FiniteDimensional F E<VAR>h : IsGalois F E<GOAL>IntermediateField.fixedField K.fixingSubgroup = K
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>K : IntermediateField F E<VAR>DecidablePred fun x => x ∈ K.fixingSubgroup<VAR>FiniteDimensional F E<VAR>IsGalois F E<GOAL>Fintype.card ↥K.fixingSubgroup = FiniteDimensional.finrank (↥K) E
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>FiniteDimensional F E<VAR>IsGalois F E<GOAL>∃ p, p.Separable ∧ Polynomial.IsSplittingField F E p
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>FiniteDimensional F E<VAR>h : IntermediateField.fixedField ⊤ = ⊥<GOAL>IsGalois F E
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>FiniteDimensional F E<VAR>h : Fintype.card (E ≃ₐ[F] E) = FiniteDimensional.finrank F E<GOAL>IsGalois F E
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>p : F[X]<VAR>hFE : FiniteDimensional F E<VAR>sp : Polynomial.IsSplittingField F E p<VAR>hp : p.Separable<VAR>K : Type u_3<VAR>Field K<VAR>Algebra F K<VAR>Algebra K E<VAR>IsScalarTower F K E<VAR>x : E<VAR>hx : x ∈ p.aroots E<VAR>Fintype (K →ₐ[F] E)<VAR>Fintype (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E)<GOAL>Fintype.card (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) = Fintype.card (K →ₐ[F] E) * FiniteDimensional.finrank K ↥K⟮x⟯
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>p : F[X]<VAR>sp : Polynomial.IsSplittingField F E p<VAR>hp : p.Separable<GOAL>IsGalois F E
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>FiniteDimensional F E<GOAL>[IsGalois F E, IntermediateField.fixedField ⊤ = ⊥, Fintype.card (E ≃ₐ[F] E) = FiniteDimensional.finrank F E, ∃ p, p.Separable ∧ Polynomial.IsSplittingField F E p].TFAE
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>f g : CategoryTheory.MonoOver X<VAR>Y : C<VAR>h : Y ⟶ X<VAR>e : f ≅ g<GOAL>f.Factors h ↔ g.Factors h
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>f : Y ⟶ X<VAR>CategoryTheory.Mono f<VAR>g : Z ⟶ X<GOAL>(CategoryTheory.Subobject.mk f).Factors g ↔ (CategoryTheory.MonoOver.mk' f).Factors g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Mono f<GOAL>(CategoryTheory.Subobject.mk f).Factors f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>P : CategoryTheory.Subobject Y<VAR>f : X ⟶ Y<GOAL>P.Factors f ↔ (CategoryTheory.Subobject.representative.obj P).Factors f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>P : CategoryTheory.Subobject X<GOAL>P.Factors P.arrow
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>P : CategoryTheory.Subobject Y<VAR>f : X ⟶ CategoryTheory.Subobject.underlying.obj P<GOAL>P.Factors (f ≫ P.arrow)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>P : CategoryTheory.Subobject Z<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>h : P.Factors g<GOAL>P.Factors (f ≫ g)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>P : CategoryTheory.Subobject Y<GOAL>P.Factors 0
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>Y Z : C<VAR>P Q : CategoryTheory.Subobject Y<VAR>f : Z ⟶ Y<VAR>h : P ≤ Q<GOAL>P.Factors f → Q.Factors f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>P : CategoryTheory.Subobject Y<VAR>f : X ⟶ Y<VAR>h : P.Factors f<GOAL>P.factorThru f h ≫ P.arrow = f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>P : CategoryTheory.Subobject X<VAR>h : P.Factors P.arrow<GOAL>P.factorThru P.arrow h = 𝟙 (CategoryTheory.Subobject.underlying.obj P)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Mono f<GOAL>(CategoryTheory.Subobject.mk f).factorThru f ⋯ = (CategoryTheory.Subobject.underlyingIso f).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>P : CategoryTheory.Subobject Y<VAR>f : X ⟶ CategoryTheory.Subobject.underlying.obj P<VAR>h : P.Factors (f ≫ P.arrow)<GOAL>P.factorThru (f ≫ P.arrow) h = f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>P : CategoryTheory.Subobject Y<VAR>f : X ⟶ Y<VAR>h : P.Factors f<GOAL>P.factorThru f h = 0 ↔ f = 0
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>P : CategoryTheory.Subobject Z<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>h : P.Factors g<GOAL>f ≫ P.factorThru g h = P.factorThru (f ≫ g) ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>P : CategoryTheory.Subobject Y<VAR>h : P.Factors 0<GOAL>P.factorThru 0 h = 0
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>Y Z : C<VAR>P Q : CategoryTheory.Subobject Y<VAR>f : Z ⟶ Y<VAR>h : P ≤ Q<VAR>w : P.Factors f<GOAL>Q.factorThru f ⋯ = P.factorThru f w ≫ P.ofLE Q h
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>P : CategoryTheory.Subobject Y<VAR>f g : X ⟶ Y<VAR>wf : P.Factors f<VAR>wg : P.Factors g<GOAL>P.Factors (f + g)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>P : CategoryTheory.Subobject Y<VAR>f g : X ⟶ Y<VAR>w : P.Factors (f + g)<VAR>wf : P.Factors f<VAR>wg : P.Factors g<GOAL>P.factorThru (f + g) w = P.factorThru f wf + P.factorThru g wg
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>P : CategoryTheory.Subobject Y<VAR>f g : X ⟶ Y<VAR>w : P.Factors (f + g)<VAR>wg : P.Factors g<GOAL>P.Factors f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>P : CategoryTheory.Subobject Y<VAR>f g : X ⟶ Y<VAR>w : P.Factors (f + g)<VAR>wg : P.Factors g<GOAL>P.factorThru (f + g) w - P.factorThru g wg = P.factorThru f ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>P : CategoryTheory.Subobject Y<VAR>f g : X ⟶ Y<VAR>w : P.Factors (f + g)<VAR>wf : P.Factors f<GOAL>P.Factors g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>P : CategoryTheory.Subobject Y<VAR>f g : X ⟶ Y<VAR>w : P.Factors (f + g)<VAR>wf : P.Factors f<GOAL>P.factorThru (f + g) w - P.factorThru f wf = P.factorThru g ⋯
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>s : Set (AddCircle T)<VAR>hs : MeasureTheory.NullMeasurableSet s MeasureTheory.volume<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>l.NeBot<VAR>u : ι → AddCircle T<VAR>hu₁ : ∀ (i : ι), u i +ᵥ s =ᵐ[MeasureTheory.volume] s<VAR>hu₂ : Filter.Tendsto (addOrderOf ∘ u) l Filter.atTop<GOAL>s =ᵐ[MeasureTheory.volume] ∅ ∨ s =ᵐ[MeasureTheory.volume] Set.univ
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>n : ℤ<VAR>hn : 1 < |n|<GOAL>Ergodic (fun y => n • y) MeasureTheory.volume
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>n : ℕ<VAR>hn : 1 < n<GOAL>Ergodic (fun y => n • y) MeasureTheory.volume
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>x : AddCircle T<VAR>n : ℤ<VAR>h : 1 < |n|<GOAL>Ergodic (fun y => n • y + x) MeasureTheory.volume
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>x : AddCircle T<VAR>n : ℕ<VAR>h : 1 < n<GOAL>Ergodic (fun y => n • y + x) MeasureTheory.volume
<VAR>K : Type u<VAR>Field K<VAR>n : ℕ<VAR>a : K<GOAL>AdjoinRoot.root (Polynomial.X ^ n - Polynomial.C a) ^ n = (AdjoinRoot.of (Polynomial.X ^ n - Polynomial.C a)) a
<VAR>K : Type u<VAR>Field K<VAR>n : ℕ<VAR>hn : 1 < n<VAR>a : K<GOAL>AdjoinRoot.root (Polynomial.X ^ n - Polynomial.C a) ≠ 0
<VAR>K : Type u<VAR>Field K<VAR>n : ℕ<VAR>a : K<VAR>hn : 0 < n<VAR>ha : a ≠ 0<GOAL>AdjoinRoot.root (Polynomial.X ^ n - Polynomial.C a) ≠ 0
<VAR>K : Type u<VAR>Field K<VAR>n : ℕ<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ n<VAR>α a : K<VAR>e : α ^ n = a<GOAL>Polynomial.Splits (RingHom.id K) (Polynomial.X ^ n - Polynomial.C a)
<VAR>K : Type u<VAR>Field K<VAR>n : ℕ<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ n<VAR>α a : K<VAR>hn : 0 < n<VAR>e : α ^ n = a<GOAL>Polynomial.X ^ n - Polynomial.C a = ∏ i ∈ Finset.range n, (Polynomial.X - Polynomial.C (ζ ^ i * α))
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>n : ℕ<VAR>ζ : R<VAR>hζ : IsPrimitiveRoot ζ n<VAR>α a : R<VAR>hn : 0 < n<VAR>e : α ^ n = a<GOAL>Polynomial.X ^ n - Polynomial.C a = ∏ i ∈ Finset.range n, (Polynomial.X - Polynomial.C (ζ ^ i * α))
<VAR>K : Type u<VAR>Field K<VAR>n : ℕ<VAR>a : K<VAR>H : Irreducible (Polynomial.X ^ n - Polynomial.C a)<GOAL>n ≠ 0
<VAR>K : Type u<VAR>Field K<VAR>n : ℕ<VAR>hn : n ≠ 1<VAR>a : K<VAR>H : Irreducible (Polynomial.X ^ n - Polynomial.C a)<GOAL>a ≠ 0
<VAR>K : Type u<VAR>Field K<VAR>n : ℕ<VAR>a : K<VAR>H : Irreducible (Polynomial.X ^ n - Polynomial.C a)<GOAL>AdjoinRoot.root (Polynomial.X ^ n - Polynomial.C a) = 0 ↔ a = 0
<VAR>K : Type u<VAR>Field K<VAR>n : ℕ<VAR>a : K<VAR>H : Irreducible (Polynomial.X ^ n - Polynomial.C a)<GOAL>AdjoinRoot.root (Polynomial.X ^ n - Polynomial.C a) ≠ 0 ↔ a ≠ 0
<VAR>K : Type u<VAR>Field K<VAR>n : ℕ<VAR>a : K<VAR>H : Irreducible (Polynomial.X ^ n - Polynomial.C a)<VAR>m : ℕ<VAR>hm : m ∣ n<VAR>hm' : m ≠ 1<VAR>b : K<GOAL>b ^ m ≠ a
<VAR>K : Type u<VAR>Field K<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>a : K<VAR>ha : ∀ (b : K), b ^ p ≠ a<GOAL>Irreducible (Polynomial.X ^ p - Polynomial.C a)
<VAR>K : Type u<VAR>Field K<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>a : K<GOAL>Irreducible (Polynomial.X ^ p - Polynomial.C a) ↔ ∀ (b : K), b ^ p ≠ a
<VAR>K : Type u<VAR>Field K<VAR>n m : ℕ<VAR>a : K<VAR>hm : Irreducible (Polynomial.X ^ m - Polynomial.C a)<VAR>hn : ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E), minpoly K x = Polynomial.X ^ m - Polynomial.C a → Irreducible (Polynomial.X ^ n - Polynomial.C (IntermediateField.AdjoinSimple.gen K x))<GOAL>Irreducible (Polynomial.X ^ (n * m) - Polynomial.C a)
<VAR>K : Type u<VAR>Field K<VAR>n : ℕ<VAR>hn : Odd n<VAR>a : K<VAR>ha : ∀ (p : ℕ), Nat.Prime p → p ∣ n → ∀ (b : K), b ^ p ≠ a<GOAL>Irreducible (Polynomial.X ^ n - Polynomial.C a)
<VAR>K : Type u<VAR>Field K<VAR>n : ℕ<VAR>hn : Odd n<VAR>a : K<GOAL>Irreducible (Polynomial.X ^ n - Polynomial.C a) ↔ ∀ (p : ℕ), Nat.Prime p → p ∣ n → ∀ (b : K), b ^ p ≠ a
<VAR>K : Type u<VAR>Field K<VAR>n : ℕ<VAR>hn : Odd n<VAR>a : K<GOAL>Irreducible (Polynomial.X ^ n - Polynomial.C a) ↔ ∀ (d : ℕ), d ∣ n → d ≠ 1 → ∀ (b : K), b ^ d ≠ a
<VAR>K : Type u<VAR>Field K<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hp' : p ≠ 2<VAR>n : ℕ<VAR>a : K<VAR>ha : ∀ (b : K), b ^ p ≠ a<GOAL>Irreducible (Polynomial.X ^ p ^ n - Polynomial.C a)
<VAR>K : Type u<VAR>Field K<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hp' : p ≠ 2<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>a : K<GOAL>Irreducible (Polynomial.X ^ p ^ n - Polynomial.C a) ↔ ∀ (b : K), b ^ p ≠ a
<VAR>K : Type u<VAR>Field K<VAR>n : ℕ<VAR>hζ : (primitiveRoots n K).Nonempty<VAR>a : K<VAR>H : Irreducible (Polynomial.X ^ n - Polynomial.C a)<GOAL>(Polynomial.X ^ n - Polynomial.C a).Separable
<VAR>K : Type u<VAR>Field K<VAR>n : ℕ<VAR>hn : 0 < n<VAR>a : K<VAR>η : ↥(rootsOfUnity ⟨n, hn⟩ K)<GOAL>((autAdjoinRootXPowSubC hn a) η) (AdjoinRoot.root (Polynomial.X ^ n - Polynomial.C a)) = ↑↑η • AdjoinRoot.root (Polynomial.X ^ n - Polynomial.C a)
<VAR>K : Type u<VAR>Field K<VAR>n : ℕ<VAR>hζ : (primitiveRoots n K).Nonempty<VAR>hn : 0 < n<VAR>a : K<VAR>H : Irreducible (Polynomial.X ^ n - Polynomial.C a)<VAR>η : ↥(rootsOfUnity ⟨n, hn⟩ K)<GOAL>((autAdjoinRootXPowSubCEquiv hζ hn H) η) (AdjoinRoot.root (Polynomial.X ^ n - Polynomial.C a)) = ↑↑η • AdjoinRoot.root (Polynomial.X ^ n - Polynomial.C a)
<VAR>K : Type u<VAR>Field K<VAR>n : ℕ<VAR>hζ : (primitiveRoots n K).Nonempty<VAR>hn : 0 < n<VAR>a : K<VAR>H : Irreducible (Polynomial.X ^ n - Polynomial.C a)<VAR>σ : K[n√a] ≃ₐ[K] K[n√a]<GOAL>↑((autAdjoinRootXPowSubCEquiv hζ hn H).symm σ) • AdjoinRoot.root (Polynomial.X ^ n - Polynomial.C a) = σ (AdjoinRoot.root (Polynomial.X ^ n - Polynomial.C a))
<VAR>K : Type u<VAR>Field K<VAR>n : ℕ<VAR>hζ : (primitiveRoots n K).Nonempty<VAR>a : K<VAR>H : Irreducible (Polynomial.X ^ n - Polynomial.C a)<GOAL>Polynomial.IsSplittingField K K[n√a] (Polynomial.X ^ n - Polynomial.C a)
<VAR>K : Type u<VAR>Field K<VAR>n : ℕ<VAR>hζ : (primitiveRoots n K).Nonempty<VAR>a : K<VAR>H : Irreducible (Polynomial.X ^ n - Polynomial.C a)<VAR>L : Type u_1<VAR>Field L<VAR>Algebra K L<VAR>Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)<VAR>α : L<VAR>hα : α ^ n = (algebraMap K L) a<GOAL>(adjoinRootXPowSubCEquiv hζ H hα) (AdjoinRoot.root (Polynomial.X ^ n - Polynomial.C a)) = α
<VAR>K : Type u<VAR>Field K<VAR>n : ℕ<VAR>hζ : (primitiveRoots n K).Nonempty<VAR>a : K<VAR>H : Irreducible (Polynomial.X ^ n - Polynomial.C a)<VAR>L : Type u_1<VAR>Field L<VAR>Algebra K L<VAR>Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)<VAR>α : L<VAR>hα : α ^ n = (algebraMap K L) a<GOAL>(adjoinRootXPowSubCEquiv hζ H hα).symm α = AdjoinRoot.root (Polynomial.X ^ n - Polynomial.C a)
<VAR>K : Type u<VAR>Field K<VAR>n : ℕ<VAR>hζ : (primitiveRoots n K).Nonempty<VAR>a : K<VAR>H : Irreducible (Polynomial.X ^ n - Polynomial.C a)<VAR>L : Type u_1<VAR>Field L<VAR>Algebra K L<VAR>Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)<VAR>α : L<VAR>hα : α ^ n = (algebraMap K L) a<GOAL>Algebra.adjoin K {α} = ⊤
<VAR>K : Type u<VAR>Field K<VAR>n : ℕ<VAR>hζ : (primitiveRoots n K).Nonempty<VAR>a : K<VAR>H : Irreducible (Polynomial.X ^ n - Polynomial.C a)<VAR>L : Type u_1<VAR>Field L<VAR>Algebra K L<VAR>Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)<VAR>α : L<VAR>hα : α ^ n = (algebraMap K L) a<GOAL>K⟮α⟯ = ⊤
<VAR>K : Type u<VAR>Field K<VAR>n : ℕ<VAR>hn : 0 < n<VAR>a : K<VAR>L : Type u_1<VAR>Field L<VAR>Algebra K L<VAR>Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)<GOAL>rootOfSplitsXPowSubC hn a L ^ n = (algebraMap K L) a
<VAR>K : Type u<VAR>Field K<VAR>n : ℕ<VAR>hζ : (primitiveRoots n K).Nonempty<VAR>hn : 0 < n<VAR>a : K<VAR>H : Irreducible (Polynomial.X ^ n - Polynomial.C a)<VAR>L : Type u_1<VAR>Field L<VAR>Algebra K L<VAR>Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)<VAR>σ : L ≃ₐ[K] L<GOAL>σ (rootOfSplitsXPowSubC hn a L) = (autEquivRootsOfUnity hζ hn H L) σ • rootOfSplitsXPowSubC hn a L
<VAR>K : Type u<VAR>Field K<VAR>n : ℕ<VAR>hζ : (primitiveRoots n K).Nonempty<VAR>hn : 0 < n<VAR>a : K<VAR>H : Irreducible (Polynomial.X ^ n - Polynomial.C a)<VAR>L : Type u_1<VAR>Field L<VAR>Algebra K L<VAR>Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)<VAR>α : L<VAR>hα : α ^ n = (algebraMap K L) a<VAR>σ : L ≃ₐ[K] L<GOAL>(autEquivRootsOfUnity hζ hn H L) σ • α = σ α
<VAR>K : Type u<VAR>Field K<VAR>n : ℕ<VAR>a : K<VAR>H : Irreducible (Polynomial.X ^ n - Polynomial.C a)<VAR>L : Type u_1<VAR>Field L<VAR>Algebra K L<VAR>Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)<VAR>α : L<VAR>hα : α ^ n = (algebraMap K L) a<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ n<VAR>m : ℤ<GOAL>((autEquivZmod H L hζ).symm (Multiplicative.ofAdd ↑m)) α = ζ ^ m • α
<VAR>K : Type u<VAR>Field K<VAR>n : ℕ<VAR>a : K<VAR>H : Irreducible (Polynomial.X ^ n - Polynomial.C a)<VAR>L : Type u_1<VAR>Field L<VAR>Algebra K L<VAR>Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)<VAR>α : L<VAR>hα : α ^ n = (algebraMap K L) a<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ n<VAR>m : ℕ<GOAL>((autEquivZmod H L hζ).symm (Multiplicative.ofAdd ↑m)) α = ζ ^ m • α
<VAR>K : Type u<VAR>Field K<VAR>n : ℕ<VAR>hζ : (primitiveRoots n K).Nonempty<VAR>a : K<VAR>H : Irreducible (Polynomial.X ^ n - Polynomial.C a)<VAR>L : Type u_1<VAR>Field L<VAR>Algebra K L<VAR>Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)<GOAL>IsCyclic (L ≃ₐ[K] L)
<VAR>K : Type u<VAR>Field K<VAR>n : ℕ<VAR>hζ : (primitiveRoots n K).Nonempty<VAR>a : K<VAR>H : Irreducible (Polynomial.X ^ n - Polynomial.C a)<VAR>L : Type u_1<VAR>Field L<VAR>Algebra K L<VAR>Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)<GOAL>IsGalois K L
<VAR>K : Type u<VAR>Field K<VAR>n : ℕ<VAR>hζ : (primitiveRoots n K).Nonempty<VAR>a : K<VAR>H : Irreducible (Polynomial.X ^ n - Polynomial.C a)<VAR>L : Type u_1<VAR>Field L<VAR>Algebra K L<VAR>Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)<GOAL>FiniteDimensional.finrank K L = n
<VAR>K : Type u<VAR>Field K<VAR>L : Type u_1<VAR>Field L<VAR>Algebra K L<VAR>IsGalois K L<VAR>FiniteDimensional K L<VAR>IsCyclic (L ≃ₐ[K] L)<VAR>hK : (primitiveRoots (FiniteDimensional.finrank K L) K).Nonempty<GOAL>∃ α, α ^ FiniteDimensional.finrank K L ∈ Set.range ⇑(algebraMap K L) ∧ K⟮α⟯ = ⊤