ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>F E : IntermediateField K L<VAR>FiniteDimensional K L<VAR>h_le : F ≤ E<VAR>h_finrank : FiniteDimensional.finrank (↥F) L ≤ FiniteDimensional.finrank (↥E) L<GOAL>F = E
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>F E : IntermediateField K L<VAR>FiniteDimensional (↥F) L<VAR>h_le : F ≤ E<VAR>h_finrank : FiniteDimensional.finrank (↥F) L ≤ FiniteDimensional.finrank (↥E) L<GOAL>F = E
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>F E : IntermediateField K L<VAR>FiniteDimensional (↥F) L<VAR>h_le : F ≤ E<VAR>h_finrank : FiniteDimensional.finrank (↥F) L = FiniteDimensional.finrank (↥E) L<GOAL>F = E
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>S : IntermediateField K L<VAR>x : ↥S<GOAL>IsAlgebraic K x ↔ IsAlgebraic K ↑x
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>S : IntermediateField K L<VAR>x : ↥S<GOAL>IsIntegral K x ↔ IsIntegral K ↑x
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>S : IntermediateField K L<VAR>x : ↥S<GOAL>minpoly K x = minpoly K ↑x
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>Algebra.IsAlgebraic K L<VAR>S : Subalgebra K L<VAR>x : L<GOAL>x ∈ subalgebraEquivIntermediateField S ↔ x ∈ S
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>Algebra.IsAlgebraic K L<VAR>S : IntermediateField K L<VAR>x : L<GOAL>x ∈ subalgebraEquivIntermediateField.symm S ↔ x ∈ S
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>Preorder τ<VAR>Zero τ<VAR>ϕ : τ → α → α<VAR>s : Set α<VAR>h : IsInvariant ϕ s<GOAL>IsFwInvariant ϕ s
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>CanonicallyOrderedAddCommMonoid τ<VAR>ϕ : τ → α → α<VAR>s : Set α<VAR>h : IsFwInvariant ϕ s<GOAL>IsInvariant ϕ s
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>CanonicallyOrderedAddCommMonoid τ<VAR>ϕ : τ → α → α<VAR>s : Set α<GOAL>IsFwInvariant ϕ s ↔ IsInvariant ϕ s
<VAR>τ : Type u_1<VAR>TopologicalSpace τ<VAR>AddMonoid τ<VAR>ContinuousAdd τ<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>self : Flow τ α<GOAL>Continuous (Function.uncurry self.toFun)
<VAR>τ : Type u_1<VAR>TopologicalSpace τ<VAR>AddMonoid τ<VAR>ContinuousAdd τ<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>self : Flow τ α<VAR>t₁ t₂ : τ<VAR>x : α<GOAL>self.toFun (t₁ + t₂) x = self.toFun t₁ (self.toFun t₂ x)
<VAR>τ : Type u_1<VAR>TopologicalSpace τ<VAR>AddMonoid τ<VAR>ContinuousAdd τ<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>self : Flow τ α<VAR>x : α<GOAL>self.toFun 0 x = x
<VAR>τ : Type u_1<VAR>AddMonoid τ<VAR>TopologicalSpace τ<VAR>ContinuousAdd τ<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>ϕ₁ ϕ₂ : Flow τ α<GOAL>(∀ (t : τ) (x : α), ϕ₁.toFun t x = ϕ₂.toFun t x) → ϕ₁ = ϕ₂
<VAR>τ : Type u_1<VAR>AddMonoid τ<VAR>TopologicalSpace τ<VAR>ContinuousAdd τ<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>ϕ : Flow τ α<VAR>β : Type u_3<VAR>TopologicalSpace β<VAR>t : β → τ<VAR>ht : Continuous t<VAR>f : β → α<VAR>hf : Continuous f<GOAL>Continuous fun x => ϕ.toFun (t x) (f x)
<VAR>τ : Type u_1<VAR>AddMonoid τ<VAR>TopologicalSpace τ<VAR>ContinuousAdd τ<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>ϕ : Flow τ α<VAR>t₁ t₂ : τ<VAR>x : α<GOAL>ϕ.toFun (t₁ + t₂) x = ϕ.toFun t₁ (ϕ.toFun t₂ x)
<VAR>τ : Type u_1<VAR>AddMonoid τ<VAR>TopologicalSpace τ<VAR>ContinuousAdd τ<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>ϕ : Flow τ α<GOAL>ϕ.toFun 0 = id
<VAR>τ : Type u_1<VAR>AddMonoid τ<VAR>TopologicalSpace τ<VAR>ContinuousAdd τ<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>ϕ : Flow τ α<VAR>x : α<GOAL>ϕ.toFun 0 x = x
<VAR>τ : Type u_1<VAR>AddCommGroup τ<VAR>TopologicalSpace τ<VAR>TopologicalAddGroup τ<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>ϕ : Flow τ α<VAR>s : Set α<GOAL>IsInvariant ϕ.toFun s ↔ ∀ (t : τ), ϕ.toFun t '' s = s
<VAR>τ : Type u_1<VAR>AddCommGroup τ<VAR>TopologicalSpace τ<VAR>TopologicalAddGroup τ<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>ϕ : Flow τ α<VAR>t : τ<GOAL>Continuous (ϕ.toFun t)
<VAR>τ : Type u_1<VAR>AddCommGroup τ<VAR>TopologicalSpace τ<VAR>TopologicalAddGroup τ<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>ϕ : Flow τ α<VAR>t : τ<VAR>s : Set α<GOAL>ϕ.toFun t '' s = ϕ.toFun (-t) ⁻¹' s
<VAR>R : Type u<VAR>CommSemiring R<VAR>f : R[X]<GOAL>f.Separable ↔ IsCoprime f (Polynomial.derivative f)
<VAR>R : Type u<VAR>CommSemiring R<VAR>f : R[X]<GOAL>f.Separable ↔ ∃ a b, a * f + b * Polynomial.derivative f = 1
<VAR>R : Type u<VAR>CommSemiring R<VAR>Nontrivial R<GOAL>¬Polynomial.Separable 0
<VAR>R : Type u<VAR>CommSemiring R<VAR>Nontrivial R<VAR>f : R[X]<VAR>h : f.Separable<GOAL>f ≠ 0
<VAR>R : Type u<VAR>CommSemiring R<GOAL>Polynomial.Separable 1
<VAR>R : Type u<VAR>CommSemiring R<VAR>Subsingleton R<VAR>f : R[X]<GOAL>f.Separable
<VAR>R : Type u<VAR>CommSemiring R<VAR>a : R<GOAL>(Polynomial.X + Polynomial.C a).Separable
<VAR>R : Type u<VAR>CommSemiring R<GOAL>Polynomial.X.Separable
<VAR>R : Type u<VAR>CommSemiring R<VAR>r : R<GOAL>(Polynomial.C r).Separable ↔ IsUnit r
<VAR>R : Type u<VAR>CommSemiring R<VAR>f g : R[X]<VAR>h : (f * g).Separable<GOAL>f.Separable
<VAR>R : Type u<VAR>CommSemiring R<VAR>f g : R[X]<VAR>h : (f * g).Separable<GOAL>g.Separable
<VAR>R : Type u<VAR>CommSemiring R<VAR>f g : R[X]<VAR>hf : f.Separable<VAR>hfg : g ∣ f<GOAL>g.Separable
<VAR>F : Type u_1<VAR>Field F<VAR>f : F[X]<VAR>hf : f.Separable<VAR>g : F[X]<GOAL>(EuclideanDomain.gcd f g).Separable
<VAR>F : Type u_1<VAR>Field F<VAR>g : F[X]<VAR>f : F[X]<VAR>hg : g.Separable<GOAL>(EuclideanDomain.gcd f g).Separable
<VAR>R : Type u<VAR>CommSemiring R<VAR>f g : R[X]<VAR>h : (f * g).Separable<GOAL>IsCoprime f g
<VAR>R : Type u<VAR>CommSemiring R<VAR>f : R[X]<VAR>n : ℕ<VAR>_h : (f ^ n).Separable<GOAL>IsUnit f ∨ f.Separable ∧ n = 1 ∨ n = 0
<VAR>R : Type u<VAR>CommSemiring R<VAR>f : R[X]<VAR>hf : ¬IsUnit f<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hfs : (f ^ n).Separable<GOAL>f.Separable ∧ n = 1
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Type v<VAR>CommSemiring S<VAR>p : R[X]<VAR>h : p.Separable<VAR>f : R →+* S<GOAL>(Polynomial.map f p).Separable
<VAR>R : Type u<VAR>CommSemiring R<VAR>f g : R[X]<VAR>ha : Associated f g<VAR>h : f.Separable<GOAL>g.Separable
<VAR>R : Type u<VAR>CommSemiring R<VAR>f g : R[X]<VAR>ha : Associated f g<GOAL>f.Separable ↔ g.Separable
<VAR>R : Type u<VAR>CommSemiring R<VAR>f g : R[X]<VAR>hf : f.Separable<VAR>hg : IsUnit g<GOAL>(f * g).Separable
<VAR>R : Type u<VAR>CommSemiring R<VAR>f g : R[X]<VAR>hf : IsUnit f<VAR>hg : g.Separable<GOAL>(f * g).Separable
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Type v<VAR>CommSemiring S<VAR>Nontrivial S<VAR>f : R →+* S<VAR>p : R[X]<VAR>h : p.Separable<VAR>x : S<VAR>hx : Polynomial.eval₂ f x p = 0<GOAL>Polynomial.eval₂ f x (Polynomial.derivative p) ≠ 0
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Type v<VAR>CommSemiring S<VAR>Nontrivial S<VAR>Algebra R S<VAR>p : R[X]<VAR>h : p.Separable<VAR>x : S<VAR>hx : (Polynomial.aeval x) p = 0<GOAL>(Polynomial.aeval x) (Polynomial.derivative p) ≠ 0
<VAR>R : Type u<VAR>CommSemiring R<VAR>p q : R[X]<VAR>hp : p.Separable<VAR>hq : q * q ∣ p<GOAL>IsUnit q
<VAR>R : Type u<VAR>CommSemiring R<VAR>p q : R[X]<VAR>hq : ¬IsUnit q<VAR>hsep : p.Separable<GOAL>multiplicity q p ≤ 1
<VAR>R : Type u<VAR>CommSemiring R<VAR>p : R[X]<VAR>hsep : p.Separable<GOAL>Squarefree p
<VAR>R : Type u<VAR>CommRing R<VAR>x : R<GOAL>(Polynomial.X - Polynomial.C x).Separable
<VAR>R : Type u<VAR>CommRing R<VAR>f g : R[X]<VAR>hf : f.Separable<VAR>hg : g.Separable<VAR>h : IsCoprime f g<GOAL>(f * g).Separable
<VAR>R : Type u<VAR>CommRing R<VAR>ι : Type u_1<VAR>f : ι → R[X]<VAR>s : Finset ι<GOAL>(∀ x ∈ s, ∀ y ∈ s, x ≠ y → IsCoprime (f x) (f y)) → (∀ x ∈ s, (f x).Separable) → (∏ x ∈ s, f x).Separable
<VAR>R : Type u<VAR>CommRing R<VAR>ι : Type u_1<VAR>Fintype ι<VAR>f : ι → R[X]<VAR>h1 : Pairwise (IsCoprime on f)<VAR>h2 : ∀ (x : ι), (f x).Separable<GOAL>(∏ x : ι, f x).Separable
<VAR>R : Type u<VAR>CommRing R<VAR>Nontrivial R<VAR>ι : Type u_1<VAR>f : ι → R<VAR>s : Finset ι<VAR>hfs : (∏ i ∈ s, (Polynomial.X - Polynomial.C (f i))).Separable<VAR>x y : ι<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>hfxy : f x = f y<GOAL>x = y
<VAR>R : Type u<VAR>CommRing R<VAR>Nontrivial R<VAR>ι : Type u_1<VAR>Fintype ι<VAR>f : ι → R<VAR>hfs : (∏ i : ι, (Polynomial.X - Polynomial.C (f i))).Separable<GOAL>Function.Injective f
<VAR>R : Type u<VAR>CommRing R<VAR>Nontrivial R<VAR>s : Multiset R<VAR>hs : (Multiset.map (fun a => Polynomial.X - Polynomial.C a) s).prod.Separable<GOAL>s.Nodup
<VAR>R : Type u<VAR>CommRing R<VAR>n : ℕ<VAR>u : Rˣ<VAR>hn : IsUnit ↑n<GOAL>(Polynomial.X ^ n - Polynomial.C ↑u).Separable
<VAR>R : Type u<VAR>CommRing R<VAR>Nontrivial R<VAR>p : R[X]<VAR>hsep : p.Separable<VAR>x : R<GOAL>Polynomial.rootMultiplicity x p ≤ 1
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>p : R[X]<VAR>hsep : p.Separable<VAR>x : R<GOAL>Multiset.count x p.roots ≤ 1
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>p : R[X]<VAR>hsep : p.Separable<GOAL>p.roots.Nodup
<VAR>F : Type u<VAR>Field F<VAR>f : F[X]<VAR>hf : Irreducible f<GOAL>f.Separable ↔ Polynomial.derivative f ≠ 0
<VAR>F : Type u<VAR>Field F<VAR>S : Type u_1<VAR>CommRing S<VAR>Nontrivial S<VAR>f : F →+* S<VAR>p : F[X]<GOAL>(Polynomial.map f p).Separable ↔ p.Separable
<VAR>F : Type u<VAR>Field F<VAR>ι : Type u_1<VAR>f : ι → F<VAR>s : Finset ι<GOAL>(∏ i ∈ s, (Polynomial.X - Polynomial.C (f i))).Separable ↔ ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y
<VAR>F : Type u<VAR>Field F<VAR>ι : Type u_1<VAR>Fintype ι<VAR>f : ι → F<GOAL>(∏ i : ι, (Polynomial.X - Polynomial.C (f i))).Separable ↔ Function.Injective f
<VAR>F : Type u<VAR>Field F<VAR>p : ℕ<VAR>HF : CharP F p<VAR>f : F[X]<VAR>hf : Irreducible f<GOAL>f.Separable ∨ ¬f.Separable ∧ ∃ g, Irreducible g ∧ (Polynomial.expand F p) g = f
<VAR>F : Type u<VAR>Field F<VAR>p : ℕ<VAR>HF : CharP F p<VAR>f : F[X]<VAR>hf : Irreducible f<VAR>hp : p ≠ 0<GOAL>∃ n g, g.Separable ∧ (Polynomial.expand F (p ^ n)) g = f
<VAR>F : Type u<VAR>Field F<VAR>p : ℕ<VAR>HF : CharP F p<VAR>f : F[X]<VAR>n : ℕ<VAR>hp : 0 < p<VAR>hf : ((Polynomial.expand F (p ^ n)) f).Separable<GOAL>IsUnit f ∨ n = 0
<VAR>F : Type u<VAR>Field F<VAR>p : ℕ<VAR>HF : CharP F p<VAR>f : F[X]<VAR>hf : Irreducible f<VAR>hp : 0 < p<VAR>n₁ : ℕ<VAR>g₁ : F[X]<VAR>hg₁ : g₁.Separable<VAR>hgf₁ : (Polynomial.expand F (p ^ n₁)) g₁ = f<VAR>n₂ : ℕ<VAR>g₂ : F[X]<VAR>hg₂ : g₂.Separable<VAR>hgf₂ : (Polynomial.expand F (p ^ n₂)) g₂ = f<GOAL>n₁ = n₂ ∧ g₁ = g₂
<VAR>F : Type u<VAR>Field F<VAR>n : ℕ<VAR>a : F<VAR>hn : ↑n ≠ 0<VAR>ha : a ≠ 0<GOAL>(Polynomial.X ^ n - Polynomial.C a).Separable
<VAR>F : Type u<VAR>Field F<VAR>n : ℕ<GOAL>(Polynomial.X ^ n - 1).Separable ↔ ↑n ≠ 0
<VAR>F : Type u<VAR>Field F<VAR>K : Type v<VAR>Field K<VAR>Algebra F K<VAR>p : F[X]<VAR>hsep : p.Separable<VAR>hsplit : Polynomial.Splits (algebraMap F K) p<GOAL>Fintype.card ↑(p.rootSet K) = p.natDegree
<VAR>F : Type u<VAR>Field F<VAR>f : F[X]<VAR>hf : f ≠ 0<VAR>h : Polynomial.Splits (RingHom.id F) f<GOAL>f.roots.Nodup ↔ f.Separable
<VAR>F : Type u<VAR>Field F<VAR>K : Type v<VAR>Field K<VAR>Algebra F K<VAR>f : F[X]<VAR>hf : f ≠ 0<VAR>h : Polynomial.Splits (algebraMap F K) f<GOAL>(f.aroots K).Nodup ↔ f.Separable
<VAR>F : Type u<VAR>Field F<VAR>K : Type v<VAR>Field K<VAR>Algebra F K<VAR>f : F[X]<VAR>hf : f ≠ 0<VAR>h : Polynomial.Splits (algebraMap F K) f<GOAL>Fintype.card ↑(f.rootSet K) = f.natDegree ↔ f.Separable
<VAR>F : Type u<VAR>Field F<VAR>K : Type v<VAR>Field K<VAR>i : F →+* K<VAR>x : F<VAR>h : F[X]<VAR>h_sep : h.Separable<VAR>h_root : Polynomial.eval x h = 0<VAR>h_splits : Polynomial.Splits i h<VAR>h_roots : ∀ y ∈ (Polynomial.map i h).roots, y = i x<GOAL>h = Polynomial.C h.leadingCoeff * (Polynomial.X - Polynomial.C x)
<VAR>F : Type u<VAR>Field F<VAR>K : Type v<VAR>Field K<VAR>i : F →+* K<VAR>f : F[X]<VAR>sep : f.Separable<VAR>sp : Polynomial.Splits i f<GOAL>∃ s, Polynomial.map i f = Polynomial.C (i f.leadingCoeff) * ∏ a ∈ s, (Polynomial.X - Polynomial.C a)
<VAR>F : Type u<VAR>Field F<VAR>CharZero F<VAR>f : F[X]<VAR>hf : Irreducible f<GOAL>f.Separable
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>CommRing F<VAR>Ring K<VAR>Algebra F K<GOAL>Algebra.IsSeparable F K ↔ ∀ (x : K), IsSeparable F x
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>CommRing F<VAR>Ring K<VAR>Algebra F K<VAR>self : Algebra.IsSeparable F K<VAR>x : K<GOAL>IsSeparable F x
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>CommRing F<VAR>Ring K<VAR>Algebra F K<VAR>Algebra.IsSeparable F K<VAR>x : K<GOAL>IsSeparable F x
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>CommRing F<VAR>Ring K<VAR>Algebra F K<VAR>x : K<VAR>h : IsSeparable F x<GOAL>IsIntegral F x
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>CommRing F<VAR>Ring K<VAR>Algebra F K<VAR>Algebra.IsSeparable F K<VAR>x : K<GOAL>IsIntegral F x
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>CommRing F<VAR>Ring K<VAR>Algebra F K<GOAL>Algebra.IsSeparable F K ↔ ∀ (x : K), IsIntegral F x ∧ IsSeparable F x
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>CommRing F<VAR>Ring K<VAR>Algebra F K<VAR>E : Type u_3<VAR>Ring E<VAR>Algebra F E<VAR>e : K ≃ₐ[F] E<VAR>Algebra.IsSeparable F K<GOAL>Algebra.IsSeparable F E
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>CommRing F<VAR>Ring K<VAR>Algebra F K<VAR>E : Type u_3<VAR>Ring E<VAR>Algebra F E<VAR>e : K ≃ₐ[F] E<GOAL>Algebra.IsSeparable F K ↔ Algebra.IsSeparable F E
<VAR>A : Type u_1<VAR>CommRing A<VAR>K : Type u_2<VAR>Field K<VAR>Algebra A K<VAR>R : Type u_3<VAR>CommRing R<VAR>Algebra A R<VAR>Algebra K R<VAR>IsScalarTower A K R<VAR>x : R<VAR>h : IsSeparable A x<GOAL>IsSeparable K x
<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>Algebra.IsSeparable F E<GOAL>Algebra.IsSeparable K 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>h : Algebra.IsSeparable F E<GOAL>Algebra.IsSeparable F K
<VAR>F : Type u_1<VAR>E : Type u_3<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>E' : Type u_4<VAR>Field E'<VAR>Algebra F E'<VAR>f : E →ₐ[F] E'<VAR>Algebra.IsSeparable F E'<GOAL>Algebra.IsSeparable F E
<VAR>A₁ : Type u_4<VAR>B₁ : Type u_5<VAR>A₂ : Type u_6<VAR>B₂ : Type u_7<VAR>Field A₁<VAR>Field B₁<VAR>Field A₂<VAR>Field B₂<VAR>Algebra A₁ B₁<VAR>Algebra A₂ B₂<VAR>e₁ : A₁ ≃+* A₂<VAR>e₂ : B₁ ≃+* B₂<VAR>he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁)<VAR>Algebra.IsSeparable A₁ B₁<GOAL>Algebra.IsSeparable A₂ B₂
<VAR>S : Type u_2<VAR>CommRing S<VAR>K : Type u_4<VAR>L : Type u_5<VAR>Field K<VAR>Field L<VAR>Algebra K S<VAR>Algebra K L<VAR>pb : PowerBasis K S<VAR>h_sep : IsSeparable K pb.gen<VAR>h_splits : Polynomial.Splits (algebraMap K L) (minpoly K pb.gen)<GOAL>Fintype.card (S →ₐ[K] L) = pb.dim
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v, u₂} D<VAR>F : C → D<GOAL>∀ (a : C), (CategoryTheory.inducedFunctor F).obj a = F a
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v, u₂} D<VAR>F : C → D<GOAL>∀ {X Y : CategoryTheory.InducedCategory D F} (f : X ⟶ Y), (CategoryTheory.inducedFunctor F).map f = f
<VAR>C : Type u₁<VAR>Z : C → Prop<VAR>self : CategoryTheory.FullSubcategory Z<GOAL>Z self.obj
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>Z : C → Prop<VAR>X : CategoryTheory.FullSubcategory Z<GOAL>CategoryTheory.CategoryStruct.id X = CategoryTheory.CategoryStruct.id X.obj
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>Z : C → Prop<VAR>X Y : CategoryTheory.FullSubcategory Z<GOAL>∀ {Z_1 : CategoryTheory.FullSubcategory Z} (f : X ⟶ Y) (g : Y ⟶ Z_1), CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>Z : C → Prop<VAR>X : CategoryTheory.FullSubcategory Z<GOAL>(CategoryTheory.fullSubcategoryInclusion Z).obj X = X.obj
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>Z : C → Prop<VAR>X Y : CategoryTheory.FullSubcategory Z<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.fullSubcategoryInclusion Z).map f = f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>Z Z' : C → Prop<VAR>h : ∀ ⦃X : C⦄, Z X → Z' X<VAR>X : CategoryTheory.FullSubcategory Z<GOAL>((CategoryTheory.FullSubcategory.map h).obj X).obj = X.obj
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>Z Z' : C → Prop<VAR>h : ∀ ⦃X : C⦄, Z X → Z' X<GOAL>∀ {X Y : CategoryTheory.FullSubcategory Z} (f : X ⟶ Y), (CategoryTheory.FullSubcategory.map h).map f = f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>Z Z' : C → Prop<VAR>h : ∀ ⦃X : C⦄, Z X → Z' X<GOAL>(CategoryTheory.FullSubcategory.map h).comp (CategoryTheory.fullSubcategoryInclusion Z') = CategoryTheory.fullSubcategoryInclusion Z
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>P : D → Prop<VAR>F : CategoryTheory.Functor C D<VAR>hF : ∀ (X : C), P (F.obj X)<VAR>X : C<GOAL>((CategoryTheory.FullSubcategory.lift P F hF).obj X).obj = F.obj X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>P : D → Prop<VAR>F : CategoryTheory.Functor C D<VAR>hF : ∀ (X : C), P (F.obj X)<GOAL>∀ {X Y : C} (f : X ⟶ Y), (CategoryTheory.FullSubcategory.lift P F hF).map f = F.map f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>P : D → Prop<VAR>F : CategoryTheory.Functor C D<VAR>hF : ∀ (X : C), P (F.obj X)<GOAL>(CategoryTheory.FullSubcategory.lift P F hF).comp (CategoryTheory.fullSubcategoryInclusion P) = F
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>P : D → Prop<VAR>F : CategoryTheory.Functor C D<VAR>hF : ∀ (X : C), P (F.obj X)<VAR>X : C<GOAL>(CategoryTheory.fullSubcategoryInclusion P).obj ((CategoryTheory.FullSubcategory.lift P F hF).obj X) = F.obj X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>P : D → Prop<VAR>F : CategoryTheory.Functor C D<VAR>hF : ∀ (X : C), P (F.obj X)<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.fullSubcategoryInclusion P).map ((CategoryTheory.FullSubcategory.lift P F hF).map f) = F.map f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>P Q : D → Prop<VAR>F : CategoryTheory.Functor C D<VAR>hF : ∀ (X : C), P (F.obj X)<VAR>h : ∀ ⦃X : D⦄, P X → Q X<GOAL>(CategoryTheory.FullSubcategory.lift P F hF).comp (CategoryTheory.FullSubcategory.map h) = CategoryTheory.FullSubcategory.lift Q F ⋯
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>Nonempty X<VAR>MeasurableSpace X<VAR>s : Set X<VAR>MeasurableSpace.CountablySeparated ↑s<VAR>f : α → α<VAR>g : α → X<VAR>h : QuasiErgodic f μ<VAR>hs : ∀ᵐ (x : α) ∂μ, g x ∈ s<VAR>hgm : MeasureTheory.NullMeasurable g μ<VAR>hg_eq : g ∘ f =ᵐ[μ] g<GOAL>∃ c, g =ᵐ[μ] Function.const α c
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>Nonempty X<VAR>MeasurableSpace X<VAR>MeasurableSpace.CountablySeparated X<VAR>f : α → α<VAR>g : α → X<VAR>h : PreErgodic f μ<VAR>hgm : Measurable g<VAR>hg_eq : g ∘ f = g<GOAL>∃ c, g =ᵐ[μ] Function.const α c
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>Nonempty X<VAR>MeasurableSpace X<VAR>MeasurableSpace.CountablySeparated X<VAR>f : α → α<VAR>g : α → X<VAR>h : QuasiErgodic f μ<VAR>hgm : MeasureTheory.NullMeasurable g μ<VAR>hg_eq : g ∘ f =ᵐ[μ] g<GOAL>∃ c, g =ᵐ[μ] Function.const α c
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>Nonempty X<VAR>MeasurableSpace X<VAR>MeasurableSpace.CountablySeparated X<VAR>f : α → α<VAR>g : α → X<VAR>h : Ergodic f μ<VAR>hgm : MeasureTheory.NullMeasurable g μ<VAR>hg_eq : g ∘ f =ᵐ[μ] g<GOAL>∃ c, g =ᵐ[μ] Function.const α c
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace X<VAR>TopologicalSpace.MetrizableSpace X<VAR>Nonempty X<VAR>f : α → α<VAR>g : α → X<VAR>h : QuasiErgodic f μ<VAR>hgm : MeasureTheory.AEStronglyMeasurable g μ<VAR>hg_eq : g ∘ f =ᵐ[μ] g<GOAL>∃ c, g =ᵐ[μ] Function.const α c
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace X<VAR>TopologicalSpace.MetrizableSpace X<VAR>Nonempty X<VAR>f : α → α<VAR>h : QuasiErgodic f μ<VAR>g : α →ₘ[μ] X<VAR>hg_eq : g.compQuasiMeasurePreserving f ⋯ = g<GOAL>∃ c, g = MeasureTheory.AEEqFun.const α c
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace X<VAR>TopologicalSpace.MetrizableSpace X<VAR>Nonempty X<VAR>f : α → α<VAR>g : α → X<VAR>h : Ergodic f μ<VAR>hgm : MeasureTheory.AEStronglyMeasurable g μ<VAR>hg_eq : g ∘ f =ᵐ[μ] g<GOAL>∃ c, g =ᵐ[μ] Function.const α c
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace X<VAR>TopologicalSpace.MetrizableSpace X<VAR>Nonempty X<VAR>f : α → α<VAR>h : Ergodic f μ<VAR>g : α →ₘ[μ] X<VAR>hg_eq : g.compMeasurePreserving f ⋯ = g<GOAL>∃ c, g = MeasureTheory.AEEqFun.const α c
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → α<VAR>μ : autoParam (MeasureTheory.Measure α) _auto✝<VAR>self : PreErgodic f μ<VAR>s : Set α<GOAL>MeasurableSet s → f ⁻¹' s = s → s =ᵐ[μ] ∅ ∨ s =ᵐ[μ] Set.univ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>hf : PreErgodic f μ<VAR>hs : MeasurableSet s<VAR>hs' : f ⁻¹' s = s<GOAL>μ s = 0 ∨ μ sᶜ = 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>hf : PreErgodic f μ<VAR>hsm : MeasurableSet s<VAR>hs : f ⁻¹' s = s<GOAL>(∀ᵐ (x : α) ∂μ, x ∈ s) ∨ ∀ᵐ (x : α) ∂μ, x ∉ s
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>hf : PreErgodic f μ<VAR>hs : MeasurableSet s<VAR>hs' : f ⁻¹' s = s<GOAL>μ s = 0 ∨ μ s = 1
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → α<VAR>μ : MeasureTheory.Measure α<VAR>n : ℕ<VAR>hf : PreErgodic f^[n] μ<GOAL>PreErgodic f μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_2<VAR>m' : MeasurableSpace β<VAR>μ' : MeasureTheory.Measure β<VAR>g : α → β<VAR>hg : MeasureTheory.MeasurePreserving g μ μ'<VAR>hf : PreErgodic f μ<VAR>f' : β → β<VAR>h_comm : g ∘ f = f' ∘ g<GOAL>PreErgodic f' μ'
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_2<VAR>m' : MeasurableSpace β<VAR>μ' : MeasureTheory.Measure β<VAR>e : α ≃ᵐ β<VAR>h : MeasureTheory.MeasurePreserving (⇑e) μ μ'<GOAL>PreErgodic (⇑e ∘ f ∘ ⇑e.symm) μ' ↔ PreErgodic f μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_2<VAR>m' : MeasurableSpace β<VAR>μ' : MeasureTheory.Measure β<VAR>e : α ≃ᵐ β<VAR>h : MeasureTheory.MeasurePreserving (⇑e) μ μ'<GOAL>Ergodic (⇑e ∘ f ∘ ⇑e.symm) μ' ↔ Ergodic f μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>hf : QuasiErgodic 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>hf : QuasiErgodic f μ<VAR>hsm : MeasureTheory.NullMeasurableSet 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>hf : QuasiErgodic f μ<VAR>hsm : MeasureTheory.NullMeasurableSet s μ<VAR>hs : f ⁻¹' s =ᵐ[μ] s<GOAL>(∀ᵐ (x : α) ∂μ, x ∈ s) ∨ ∀ᵐ (x : α) ∂μ, x ∉ s
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → α<VAR>μ : MeasureTheory.Measure α<VAR>hf : Ergodic f μ<GOAL>QuasiErgodic f μ
<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>hf : Ergodic f μ<VAR>hs : MeasurableSet s<VAR>hs' : s ≤ᵐ[μ] f ⁻¹' s<VAR>h_fin : μ s ≠ ⊤<GOAL>s =ᵐ[μ] ∅ ∨ s =ᵐ[μ] Set.univ