ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>hf : Ergodic f μ<VAR>hs : MeasurableSet s<VAR>hs' : f '' s ≤ᵐ[μ] s<VAR>h_fin : μ s ≠ ⊤<GOAL>s =ᵐ[μ] ∅ ∨ s =ᵐ[μ] Set.univ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hf : Ergodic f μ<VAR>hs : MeasurableSet s<VAR>hs' : f ⁻¹' s ≤ᵐ[μ] s<GOAL>s =ᵐ[μ] ∅ ∨ s =ᵐ[μ] Set.univ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hf : Ergodic f μ<VAR>hs : MeasurableSet s<VAR>hs' : s ≤ᵐ[μ] f ⁻¹' s<GOAL>s =ᵐ[μ] ∅ ∨ s =ᵐ[μ] Set.univ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hf : Ergodic f μ<VAR>hs : MeasurableSet s<VAR>hs' : f '' s ≤ᵐ[μ] s<GOAL>s =ᵐ[μ] ∅ ∨ s =ᵐ[μ] Set.univ
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>self : CategoryTheory.SplitMono f<GOAL>CategoryTheory.CategoryStruct.comp f self.retraction = CategoryTheory.CategoryStruct.id X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>self : CategoryTheory.IsSplitMono f<GOAL>Nonempty (CategoryTheory.SplitMono f)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>sm : CategoryTheory.SplitMono f<GOAL>CategoryTheory.IsSplitMono f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>self : CategoryTheory.SplitEpi f<GOAL>CategoryTheory.CategoryStruct.comp self.section_ f = CategoryTheory.CategoryStruct.id Y
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>self : CategoryTheory.IsSplitEpi f<GOAL>Nonempty (CategoryTheory.SplitEpi f)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>se : CategoryTheory.SplitEpi f<GOAL>CategoryTheory.IsSplitEpi f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>hf : CategoryTheory.IsSplitMono f<GOAL>CategoryTheory.CategoryStruct.comp f (CategoryTheory.retraction f) = CategoryTheory.CategoryStruct.id X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsSplitMono f<VAR>CategoryTheory.Epi f<GOAL>CategoryTheory.IsIso f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>hf : CategoryTheory.IsSplitEpi f<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.section_ f) f = CategoryTheory.CategoryStruct.id Y
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Mono f<VAR>CategoryTheory.IsSplitEpi f<GOAL>CategoryTheory.IsIso f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>sm : CategoryTheory.SplitMono f<GOAL>CategoryTheory.Mono f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>se : CategoryTheory.SplitEpi f<GOAL>CategoryTheory.Epi f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>hf : CategoryTheory.SplitMono f<VAR>CategoryTheory.Mono hf.retraction<GOAL>CategoryTheory.IsIso f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>hf : CategoryTheory.IsSplitMono f<VAR>hf' : CategoryTheory.Mono (CategoryTheory.retraction f)<GOAL>CategoryTheory.IsIso f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>hf : CategoryTheory.SplitEpi f<VAR>CategoryTheory.Epi hf.section_<GOAL>CategoryTheory.IsIso f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>hf : CategoryTheory.IsSplitEpi f<VAR>hf' : CategoryTheory.Epi (CategoryTheory.section_ f)<GOAL>CategoryTheory.IsIso f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>self : CategoryTheory.SplitMonoCategory C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Mono f<GOAL>CategoryTheory.IsSplitMono f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>self : CategoryTheory.SplitEpiCategory C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Epi f<GOAL>CategoryTheory.IsSplitEpi f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.SplitMonoCategory C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Mono f<GOAL>CategoryTheory.IsSplitMono f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.SplitEpiCategory C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Epi f<GOAL>CategoryTheory.IsSplitEpi f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>sm : CategoryTheory.SplitMono f<VAR>F : CategoryTheory.Functor C D<GOAL>(sm.map F).retraction = F.map sm.retraction
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>se : CategoryTheory.SplitEpi f<VAR>F : CategoryTheory.Functor C D<GOAL>(se.map F).section_ = F.map se.section_
<VAR>K : Type u_1<VAR>Field K<VAR>p q : ℕ<VAR>CharP K p<VAR>h : p ∣ q<GOAL>(Polynomial.X ^ q - Polynomial.X).Separable
<VAR>p : ℕ<VAR>h_prime : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>h : n ≠ 0<GOAL>FiniteDimensional.finrank (ZMod p) (GaloisField p n) = n
<VAR>p : ℕ<VAR>h_prime : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>h : n ≠ 0<GOAL>Fintype.card (GaloisField p n) = p ^ n
<VAR>p : ℕ<VAR>h_prime : Fact (Nat.Prime p)<GOAL>Polynomial.Splits (RingHom.id (ZMod p)) (Polynomial.X ^ p - Polynomial.X)
<VAR>p : ℕ<VAR>h_prime : Fact (Nat.Prime p)<VAR>K : Type u_1<VAR>Field K<VAR>Fintype K<VAR>Algebra (ZMod p) K<GOAL>Polynomial.Splits (algebraMap (ZMod p) K) (Polynomial.X ^ Fintype.card K - Polynomial.X)
<VAR>p : ℕ<VAR>h_prime : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>K : Type u_1<VAR>Field K<VAR>Fintype K<VAR>Algebra (ZMod p) K<VAR>h : Fintype.card K = p ^ n<GOAL>Polynomial.IsSplittingField (ZMod p) K (Polynomial.X ^ p ^ n - Polynomial.X)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α → β<VAR>μa : autoParam (MeasureTheory.Measure α) _auto✝<VAR>μb : autoParam (MeasureTheory.Measure β) _auto✝¹<VAR>self : MeasureTheory.MeasurePreserving f μa μb<GOAL>MeasureTheory.Measure.map f μa = μb
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α → β<VAR>μa : autoParam (MeasureTheory.Measure α) _auto✝<VAR>μb : autoParam (MeasureTheory.Measure β) _auto✝¹<VAR>self : MeasureTheory.MeasurePreserving f μa μb<GOAL>Measurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α → β<VAR>h : Measurable f<VAR>μa : MeasureTheory.Measure α<GOAL>MeasureTheory.MeasurePreserving f μa (MeasureTheory.Measure.map f μa)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>MeasureTheory.MeasurePreserving id μ μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μa : MeasureTheory.Measure α<VAR>μb : MeasureTheory.Measure β<VAR>f : α → β<VAR>hf : MeasureTheory.MeasurePreserving f μa μb<GOAL>AEMeasurable f μa
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>IsEmpty β<VAR>f : α → β<VAR>μa : MeasureTheory.Measure α<VAR>μb : MeasureTheory.Measure β<GOAL>MeasureTheory.MeasurePreserving f μa μb
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>e : α ≃ᵐ β<VAR>μa : MeasureTheory.Measure α<VAR>μb : MeasureTheory.Measure β<VAR>h : MeasureTheory.MeasurePreserving (⇑e) μa μb<GOAL>MeasureTheory.MeasurePreserving (⇑e.symm) μb μa
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μa : MeasureTheory.Measure α<VAR>μb : MeasureTheory.Measure β<VAR>f : α → β<VAR>hf : MeasureTheory.MeasurePreserving f μa μb<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>MeasureTheory.MeasurePreserving f (μa.restrict (f ⁻¹' s)) (μb.restrict s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μa : MeasureTheory.Measure α<VAR>μb : MeasureTheory.Measure β<VAR>f : α → β<VAR>hf : MeasureTheory.MeasurePreserving f μa μb<VAR>h₂ : MeasurableEmbedding f<VAR>s : Set β<GOAL>MeasureTheory.MeasurePreserving f (μa.restrict (f ⁻¹' s)) (μb.restrict s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μa : MeasureTheory.Measure α<VAR>μb : MeasureTheory.Measure β<VAR>f : α → β<VAR>hf : MeasureTheory.MeasurePreserving f μa μb<VAR>h₂ : MeasurableEmbedding f<VAR>s : Set α<GOAL>MeasureTheory.MeasurePreserving f (μa.restrict s) (μb.restrict (f '' s))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>MeasurableSpace γ<VAR>μa : MeasureTheory.Measure α<VAR>μb : MeasureTheory.Measure β<VAR>f : α → β<VAR>hf : MeasureTheory.MeasurePreserving f μa μb<VAR>h₂ : MeasurableEmbedding f<VAR>g : β → γ<GOAL>AEMeasurable (g ∘ f) μa ↔ AEMeasurable g μb
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μa : MeasureTheory.Measure α<VAR>μb : MeasureTheory.Measure β<VAR>f : α → β<VAR>hf : MeasureTheory.MeasurePreserving f μa μb<GOAL>MeasureTheory.Measure.QuasiMeasurePreserving f μa μb
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>MeasurableSpace γ<VAR>μa : MeasureTheory.Measure α<VAR>μb : MeasureTheory.Measure β<VAR>μc : MeasureTheory.Measure γ<VAR>g : β → γ<VAR>f : α → β<VAR>hg : MeasureTheory.MeasurePreserving g μb μc<VAR>hf : MeasureTheory.MeasurePreserving f μa μb<GOAL>MeasureTheory.MeasurePreserving (g ∘ f) μa μc
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>MeasurableSpace γ<VAR>e : α ≃ᵐ β<VAR>e' : β ≃ᵐ γ<VAR>μa : MeasureTheory.Measure α<VAR>μb : MeasureTheory.Measure β<VAR>μc : MeasureTheory.Measure γ<VAR>h : MeasureTheory.MeasurePreserving (⇑e) μa μb<VAR>h' : MeasureTheory.MeasurePreserving (⇑e') μb μc<GOAL>MeasureTheory.MeasurePreserving (⇑(e.trans e')) μa μc
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>MeasurableSpace γ<VAR>μa : MeasureTheory.Measure α<VAR>μb : MeasureTheory.Measure β<VAR>μc : MeasureTheory.Measure γ<VAR>g : α → β<VAR>e : β ≃ᵐ γ<VAR>h : MeasureTheory.MeasurePreserving (⇑e) μb μc<GOAL>MeasureTheory.MeasurePreserving (⇑e ∘ g) μa μc ↔ MeasureTheory.MeasurePreserving g μa μb
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>MeasurableSpace γ<VAR>μa : MeasureTheory.Measure α<VAR>μb : MeasureTheory.Measure β<VAR>μc : MeasureTheory.Measure γ<VAR>g : α → β<VAR>e : γ ≃ᵐ α<VAR>h : MeasureTheory.MeasurePreserving (⇑e) μc μa<GOAL>MeasureTheory.MeasurePreserving (g ∘ ⇑e) μc μb ↔ MeasureTheory.MeasurePreserving g μa μb
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μa : MeasureTheory.Measure α<VAR>μb : MeasureTheory.Measure β<VAR>f : α → β<VAR>hf : MeasureTheory.MeasurePreserving f μa μb<VAR>MeasureTheory.SigmaFinite μb<GOAL>MeasureTheory.SigmaFinite μa
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μa : MeasureTheory.Measure α<VAR>μb : MeasureTheory.Measure β<VAR>f : α → β<VAR>hf : MeasureTheory.MeasurePreserving f μa μb<VAR>s : Set β<VAR>hs : MeasureTheory.NullMeasurableSet s μb<GOAL>μa (f ⁻¹' s) = μb s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μa : MeasureTheory.Measure α<VAR>μb : MeasureTheory.Measure β<VAR>f : α → β<VAR>hf : MeasureTheory.MeasurePreserving f μa μb<VAR>hfe : MeasurableEmbedding f<VAR>s : Set β<GOAL>μa (f ⁻¹' s) = μb s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μa : MeasureTheory.Measure α<VAR>μb : MeasureTheory.Measure β<VAR>f : α ≃ᵐ β<VAR>hf : MeasureTheory.MeasurePreserving (⇑f) μa μb<VAR>s : Set β<GOAL>μa (⇑f ⁻¹' s) = μb s
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μa : MeasureTheory.Measure α<VAR>f : α → α<VAR>hf : MeasureTheory.MeasurePreserving f μa μa<VAR>n : ℕ<GOAL>MeasureTheory.MeasurePreserving f^[n] μa μa
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → α<VAR>s : Set α<VAR>hf : MeasureTheory.MeasurePreserving f μ μ<VAR>hs : MeasureTheory.NullMeasurableSet s μ<VAR>n : ℕ<GOAL>μ (symmDiff s (f^[n] ⁻¹' s)) ≤ n • μ (symmDiff s (f ⁻¹' s))
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → α<VAR>s : Set α<VAR>hf : MeasureTheory.MeasurePreserving f μ μ<VAR>hs : MeasureTheory.NullMeasurableSet s μ<VAR>n : ℕ<VAR>hvol : μ Set.univ < ↑n * μ s<GOAL>∃ x ∈ s, ∃ m ∈ Set.Ioo 0 n, f^[m] x ∈ s
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → α<VAR>s : Set α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hf : MeasureTheory.MeasurePreserving f μ μ<VAR>hs : MeasureTheory.NullMeasurableSet s μ<VAR>hs' : μ s ≠ 0<GOAL>∃ x ∈ s, ∃ m, m ≠ 0 ∧ f^[m] x ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>e : α ≃ᵐ β<GOAL>MeasureTheory.MeasurePreserving (⇑e.symm) (MeasureTheory.Measure.map (⇑e) μ) μ
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>self : CategoryTheory.WellPowered C<VAR>X : C<GOAL>Small.{v, max u₁ v} (CategoryTheory.Subobject X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>X : C<GOAL>CategoryTheory.EssentiallySmall.{v, v, max u₁ v} (CategoryTheory.MonoOver X) ↔ Small.{v, max u₁ v} (CategoryTheory.Subobject X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>h : ∀ (X : C), CategoryTheory.EssentiallySmall.{v, v, max u₁ v} (CategoryTheory.MonoOver X)<GOAL>CategoryTheory.WellPowered C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v, u₂} D<VAR>e : C ≌ D<VAR>CategoryTheory.WellPowered C<GOAL>CategoryTheory.WellPowered D
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v, u₂} D<VAR>e : C ≌ D<GOAL>CategoryTheory.WellPowered C ↔ CategoryTheory.WellPowered D
<VAR>M : Type u<VAR>Monoid M<VAR>F : Type v<VAR>Field F<VAR>MulSemiringAction M F<VAR>S : Subfield F<VAR>self : IsInvariantSubfield M S<VAR>m : M<VAR>x : F<GOAL>x ∈ S → m • x ∈ S
<VAR>M : Type u<VAR>Monoid M<VAR>F : Type v<VAR>Field F<VAR>MulSemiringAction M F<VAR>m : M<VAR>x : ↥(FixedPoints.subfield M F)<GOAL>m • x = x
<VAR>M : Type u<VAR>Monoid M<VAR>F : Type v<VAR>Field F<VAR>MulSemiringAction M F<VAR>m : M<VAR>p : Polynomial ↥(FixedPoints.subfield M F)<GOAL>m • p = p
<VAR>M : Type u<VAR>Monoid M<VAR>F : Type v<VAR>Field F<VAR>MulSemiringAction M F<GOAL>algebraMap (↥(FixedPoints.subfield M F)) F = (FixedPoints.subfield M F).subtype
<VAR>G : Type u<VAR>Group G<VAR>F : Type v<VAR>Field F<VAR>MulSemiringAction G F<VAR>s : Finset F<GOAL>(LinearIndependent ↥(FixedPoints.subfield G F) fun (i : ↑↑s) => ↑i) → LinearIndependent F fun (i : ↑↑s) => (MulAction.toFun G F) ↑i
<VAR>G : Type u<VAR>Group G<VAR>F : Type v<VAR>Field F<VAR>MulSemiringAction G F<VAR>Fintype G<VAR>x : F<GOAL>(FixedPoints.minpoly G F x).Monic
<VAR>G : Type u<VAR>Group G<VAR>F : Type v<VAR>Field F<VAR>MulSemiringAction G F<VAR>Fintype G<VAR>x : F<GOAL>Polynomial.eval₂ (FixedPoints.subfield G F).subtype x (FixedPoints.minpoly G F x) = 0
<VAR>G : Type u<VAR>Group G<VAR>F : Type v<VAR>Field F<VAR>MulSemiringAction G F<VAR>Fintype G<VAR>x : F<GOAL>FixedPoints.minpoly G F x ≠ 1
<VAR>G : Type u<VAR>Group G<VAR>F : Type v<VAR>Field F<VAR>MulSemiringAction G F<VAR>Fintype G<VAR>x : F<VAR>f : Polynomial ↥(FixedPoints.subfield G F)<VAR>hf : Polynomial.eval₂ (FixedPoints.subfield G F).subtype x f = 0<GOAL>FixedPoints.minpoly G F x ∣ f
<VAR>G : Type u<VAR>Group G<VAR>F : Type v<VAR>Field F<VAR>MulSemiringAction G F<VAR>Fintype G<VAR>x : F<VAR>f g : Polynomial ↥(FixedPoints.subfield G F)<VAR>hf : f.Monic<VAR>hg : g.Monic<VAR>hfg : f * g = FixedPoints.minpoly G F x<GOAL>f = 1 ∨ g = 1
<VAR>G : Type u<VAR>Group G<VAR>F : Type v<VAR>Field F<VAR>MulSemiringAction G F<VAR>Fintype G<VAR>x : F<GOAL>Irreducible (FixedPoints.minpoly G F x)
<VAR>G : Type u<VAR>Group G<VAR>F : Type v<VAR>Field F<VAR>MulSemiringAction G F<VAR>Finite G<VAR>x : F<GOAL>IsIntegral (↥(FixedPoints.subfield G F)) x
<VAR>G : Type u<VAR>Group G<VAR>F : Type v<VAR>Field F<VAR>MulSemiringAction G F<VAR>Fintype G<VAR>x : F<GOAL>FixedPoints.minpoly G F x = minpoly (↥(FixedPoints.subfield G F)) x
<VAR>G : Type u<VAR>Group G<VAR>F : Type v<VAR>Field F<VAR>MulSemiringAction G F<VAR>Fintype G<GOAL>Module.rank (↥(FixedPoints.subfield G F)) F ≤ ↑(Fintype.card G)
<VAR>G : Type u<VAR>Group G<VAR>F : Type v<VAR>Field F<VAR>MulSemiringAction G F<VAR>Fintype G<GOAL>FiniteDimensional.finrank (↥(FixedPoints.subfield G F)) F ≤ Fintype.card G
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Ring A<VAR>Algebra R A<VAR>CommRing B<VAR>IsDomain B<VAR>Algebra R B<GOAL>LinearIndependent B AlgHom.toLinearMap
<VAR>K : Type u<VAR>V : Type v<VAR>W : Type w<VAR>Field K<VAR>Field V<VAR>Algebra K V<VAR>FiniteDimensional K V<VAR>Field W<VAR>Algebra K W<GOAL>Cardinal.mk (V →ₐ[K] W) ≤ ↑(FiniteDimensional.finrank W (V →ₗ[K] W))
<VAR>K : Type u<VAR>V : Type v<VAR>Field K<VAR>Field V<VAR>Algebra K V<VAR>FiniteDimensional K V<GOAL>Fintype.card (V →ₐ[K] V) ≤ FiniteDimensional.finrank V (V →ₗ[K] V)
<VAR>G : Type u<VAR>F : Type v<VAR>Group G<VAR>Field F<VAR>Fintype G<VAR>MulSemiringAction G F<VAR>FaithfulSMul G F<GOAL>FiniteDimensional.finrank (↥(FixedPoints.subfield G F)) F = Fintype.card G
<VAR>G : Type u<VAR>F : Type v<VAR>Group G<VAR>Field F<VAR>Finite G<VAR>MulSemiringAction G F<VAR>FaithfulSMul G F<GOAL>Function.Bijective (MulSemiringAction.toAlgHom (↥(FixedPoints.subfield G F)) F)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Polynomial R<VAR>x : S<GOAL>P.newtonMap x = x - Ring.inverse ((Polynomial.aeval x) (Polynomial.derivative P)) * (Polynomial.aeval x) P
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Polynomial R<VAR>x : S<VAR>h : IsUnit ((Polynomial.aeval x) (Polynomial.derivative P))<GOAL>P.newtonMap x = x - ↑h.unit⁻¹ * (Polynomial.aeval x) P
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Polynomial R<VAR>x : S<VAR>h : ¬IsUnit ((Polynomial.aeval x) (Polynomial.derivative P))<GOAL>P.newtonMap x = x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Polynomial R<VAR>x : S<VAR>h : IsNilpotent ((Polynomial.aeval x) P)<VAR>n : ℕ<GOAL>IsNilpotent (P.newtonMap^[n] x - x)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Polynomial R<VAR>x : S<VAR>h : (Polynomial.aeval x) P = 0<GOAL>Function.IsFixedPt P.newtonMap x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Polynomial R<VAR>x : S<VAR>h : IsUnit ((Polynomial.aeval x) (Polynomial.derivative P))<GOAL>Function.IsFixedPt P.newtonMap x ↔ (Polynomial.aeval x) P = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Polynomial R<VAR>x : S<VAR>h : IsNilpotent ((Polynomial.aeval x) P)<VAR>h' : IsUnit ((Polynomial.aeval x) (Polynomial.derivative P))<VAR>n : ℕ<GOAL>(Polynomial.aeval x) P ^ 2 ^ n ∣ (Polynomial.aeval (P.newtonMap^[n] x)) P
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Polynomial R<VAR>x : S<VAR>h : IsNilpotent ((Polynomial.aeval x) P)<VAR>h' : IsUnit ((Polynomial.aeval x) (Polynomial.derivative P))<GOAL>∃! r, IsNilpotent (x - r) ∧ (Polynomial.aeval r) P = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>self : X ≅ Y<GOAL>CategoryTheory.CategoryStruct.comp self.inv self.hom = CategoryTheory.CategoryStruct.id Y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>self : X ≅ Y<GOAL>CategoryTheory.CategoryStruct.comp self.hom self.inv = CategoryTheory.CategoryStruct.id X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>α β : X ≅ Y<VAR>w : α.hom = β.hom<GOAL>α = β
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>α : X ≅ Y<GOAL>α.symm.hom = α.inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>α : X ≅ Y<GOAL>α.symm.inv = α.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>hom : X ⟶ Y<VAR>inv : Y ⟶ X<VAR>hom_inv_id : CategoryTheory.CategoryStruct.comp hom inv = CategoryTheory.CategoryStruct.id X<VAR>inv_hom_id : CategoryTheory.CategoryStruct.comp inv hom = CategoryTheory.CategoryStruct.id Y<GOAL>{ hom := hom, inv := inv, hom_inv_id := hom_inv_id, inv_hom_id := inv_hom_id }.symm = { hom := inv, inv := hom, hom_inv_id := inv_hom_id, inv_hom_id := hom_inv_id }
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>α : X ≅ Y<GOAL>α.symm.symm = α
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>α β : X ≅ Y<GOAL>α.symm = β.symm ↔ α = β
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<GOAL>Nonempty (X ≅ Y) ↔ Nonempty (Y ≅ X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<GOAL>(CategoryTheory.Iso.refl X).hom = CategoryTheory.CategoryStruct.id X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<GOAL>(CategoryTheory.Iso.refl X).inv = CategoryTheory.CategoryStruct.id X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<GOAL>Nonempty (X ≅ X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<GOAL>(CategoryTheory.Iso.refl X).symm = CategoryTheory.Iso.refl X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>α : X ≅ Y<VAR>β : Y ≅ Z<GOAL>(α ≪≫ β).inv = CategoryTheory.CategoryStruct.comp β.inv α.inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>α : X ≅ Y<VAR>β : Y ≅ Z<GOAL>(α ≪≫ β).hom = CategoryTheory.CategoryStruct.comp α.hom β.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {a b c : C} (α : a ≅ b) (β : b ≅ c), Trans.trans α β = α ≪≫ β
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>hom : X ⟶ Y<VAR>inv : Y ⟶ X<VAR>hom_inv_id : CategoryTheory.CategoryStruct.comp hom inv = CategoryTheory.CategoryStruct.id X<VAR>inv_hom_id : CategoryTheory.CategoryStruct.comp inv hom = CategoryTheory.CategoryStruct.id Y<VAR>hom' : Y ⟶ Z<VAR>inv' : Z ⟶ Y<VAR>hom_inv_id' : CategoryTheory.CategoryStruct.comp hom' inv' = CategoryTheory.CategoryStruct.id Y<VAR>inv_hom_id' : CategoryTheory.CategoryStruct.comp inv' hom' = CategoryTheory.CategoryStruct.id Z<VAR>hom_inv_id'' : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp hom hom') (CategoryTheory.CategoryStruct.comp inv' inv) = CategoryTheory.CategoryStruct.id X<VAR>inv_hom_id'' : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp inv' inv) (CategoryTheory.CategoryStruct.comp hom hom') = CategoryTheory.CategoryStruct.id Z<GOAL>{ hom := hom, inv := inv, hom_inv_id := hom_inv_id, inv_hom_id := inv_hom_id } ≪≫ { hom := hom', inv := inv', hom_inv_id := hom_inv_id', inv_hom_id := inv_hom_id' } = { hom := CategoryTheory.CategoryStruct.comp hom hom', inv := CategoryTheory.CategoryStruct.comp inv' inv, hom_inv_id := hom_inv_id'', inv_hom_id := inv_hom_id'' }
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>α : X ≅ Y<VAR>β : Y ≅ Z<GOAL>(α ≪≫ β).symm = β.symm ≪≫ α.symm
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z Z' : C<VAR>α : X ≅ Y<VAR>β : Y ≅ Z<VAR>γ : Z ≅ Z'<GOAL>(α ≪≫ β) ≪≫ γ = α ≪≫ β ≪≫ γ
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>α : X ≅ Y<GOAL>CategoryTheory.Iso.refl X ≪≫ α = α
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>α : X ≅ Y<GOAL>α ≪≫ CategoryTheory.Iso.refl Y = α
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>α : X ≅ Y<GOAL>α.symm ≪≫ α = CategoryTheory.Iso.refl Y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>α : X ≅ Y<GOAL>α ≪≫ α.symm = CategoryTheory.Iso.refl X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>α : X ≅ Y<VAR>β : Y ≅ Z<GOAL>α.symm ≪≫ α ≪≫ β = β
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>α : X ≅ Y<VAR>β : X ≅ Z<GOAL>α ≪≫ α.symm ≪≫ β = β
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>α : X ≅ Y<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>CategoryTheory.CategoryStruct.comp α.inv f = g ↔ f = CategoryTheory.CategoryStruct.comp α.hom g