ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>Fintype K<VAR>Fintype σ<VAR>CommRing K<VAR>a : σ → K<GOAL>(MvPolynomial.eval a) (MvPolynomial.indicator a) = 1
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>Fintype K<VAR>Fintype σ<VAR>CommRing K<VAR>c : σ → K<GOAL>(MvPolynomial.indicator c).degrees ≤ ∑ s : σ, (Fintype.card K - 1) • {s}
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>Fintype K<VAR>Fintype σ<VAR>CommRing K<VAR>c : σ → K<GOAL>MvPolynomial.indicator c ∈ MvPolynomial.restrictDegree σ K (Fintype.card K - 1)
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>Fintype K<VAR>Fintype σ<VAR>Field K<VAR>a b : σ → K<VAR>h : a ≠ b<GOAL>(MvPolynomial.eval a) (MvPolynomial.indicator b) = 0
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>CommSemiring K<VAR>p : MvPolynomial σ K<VAR>e : σ → K<GOAL>(MvPolynomial.evalₗ K σ) p e = (MvPolynomial.eval e) p
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>Field K<VAR>Fintype K<VAR>Finite σ<GOAL>Submodule.map (MvPolynomial.evalₗ K σ) (MvPolynomial.restrictDegree σ K (Fintype.card K - 1)) = ⊤
<VAR>σ K : Type u<VAR>Fintype K<VAR>Field K<VAR>Fintype σ<GOAL>Module.rank K (MvPolynomial.R σ K) = ↑(Fintype.card (σ → K))
<VAR>σ K : Type u<VAR>Fintype K<VAR>Field K<VAR>Fintype σ<GOAL>FiniteDimensional.finrank K (MvPolynomial.R σ K) = Fintype.card (σ → K)
<VAR>σ K : Type u<VAR>Fintype K<VAR>Field K<VAR>Finite σ<GOAL>LinearMap.range (MvPolynomial.evalᵢ σ K) = ⊤
<VAR>σ K : Type u<VAR>Fintype K<VAR>Field K<VAR>Finite σ<GOAL>LinearMap.ker (MvPolynomial.evalᵢ σ K) = ⊥
<VAR>σ K : Type u<VAR>Fintype K<VAR>Field K<VAR>Finite σ<VAR>p : MvPolynomial σ K<VAR>h : ∀ (v : σ → K), (MvPolynomial.eval v) p = 0<VAR>hp : p ∈ MvPolynomial.restrictDegree σ K (Fintype.card K - 1)<GOAL>p = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>R : Type u_3<VAR>DivisionSemiring R<VAR>CharZero R<VAR>AddCommMonoid E<VAR>TopologicalSpace E<VAR>Module R E<VAR>f : α → α<VAR>x : α<VAR>h : Function.IsFixedPt f x<VAR>g : α → E<GOAL>Filter.Tendsto (fun x_1 => birkhoffAverage R f g x_1 x) Filter.atTop (𝓝 (g x))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>f : α → α<VAR>g : α → E<VAR>n : ℕ<VAR>x : α<GOAL>dist (birkhoffSum f g n (f x)) (birkhoffSum f g n x) = dist (g (f^[n] x)) (g x)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>f : α → α<VAR>g : α → E<VAR>n : ℕ<VAR>x y : α<GOAL>dist (birkhoffSum f g n x) (birkhoffSum f g n y) ≤ ∑ k ∈ Finset.range n, dist (g (f^[k] x)) (g (f^[k] y))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>Module 𝕜 E<VAR>BoundedSMul 𝕜 E<VAR>f : α → α<VAR>g : α → E<VAR>n : ℕ<VAR>x y : α<GOAL>dist (birkhoffAverage 𝕜 f g n x) (birkhoffAverage 𝕜 f g n y) = dist (birkhoffSum f g n x) (birkhoffSum f g n y) / ↑n
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>Module 𝕜 E<VAR>BoundedSMul 𝕜 E<VAR>f : α → α<VAR>g : α → E<VAR>n : ℕ<VAR>x y : α<GOAL>dist (birkhoffAverage 𝕜 f g n x) (birkhoffAverage 𝕜 f g n y) ≤ (∑ k ∈ Finset.range n, dist (g (f^[k] x)) (g (f^[k] y))) / ↑n
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>Module 𝕜 E<VAR>BoundedSMul 𝕜 E<VAR>f : α → α<VAR>g : α → E<VAR>n : ℕ<VAR>x : α<GOAL>dist (birkhoffAverage 𝕜 f g n (f x)) (birkhoffAverage 𝕜 f g n x) = dist (g (f^[n] x)) (g x) / ↑n
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>Module 𝕜 E<VAR>BoundedSMul 𝕜 E<VAR>f : α → α<VAR>g : α → E<VAR>x : α<VAR>h : Bornology.IsBounded (Set.range fun x_1 => g (f^[x_1] x))<GOAL>Filter.Tendsto (fun n => birkhoffAverage 𝕜 f g n (f x) - birkhoffAverage 𝕜 f g n x) Filter.atTop (𝓝 0)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>Module 𝕜 E<VAR>BoundedSMul 𝕜 E<VAR>g : α → E<VAR>h : Bornology.IsBounded (Set.range g)<VAR>f : α → α<VAR>x : α<GOAL>Filter.Tendsto (fun n => birkhoffAverage 𝕜 f g n (f x) - birkhoffAverage 𝕜 f g n x) Filter.atTop (𝓝 0)
<VAR>𝕜 : Type u_1<VAR>X : Type u_2<VAR>E : Type u_3<VAR>PseudoEMetricSpace X<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : X → X<VAR>g : X → E<VAR>hf : LipschitzWith 1 f<VAR>hg : UniformContinuous g<GOAL>UniformEquicontinuous (birkhoffAverage 𝕜 f g)
<VAR>𝕜 : Type u_1<VAR>X : Type u_2<VAR>E : Type u_3<VAR>PseudoEMetricSpace X<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : X → X<VAR>g l : X → E<VAR>hf : LipschitzWith 1 f<VAR>hg : UniformContinuous g<VAR>hl : Continuous l<GOAL>IsClosed {x | Filter.Tendsto (fun x_1 => birkhoffAverage 𝕜 f g x_1 x) Filter.atTop (𝓝 (l x))}
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>T2Space α<VAR>f : α → α<VAR>x y : α<VAR>hy : Filter.Tendsto (fun n => f^[n] x) Filter.atTop (𝓝 y)<VAR>hf : ContinuousAt f y<GOAL>Function.IsFixedPt f y
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>T2Space α<VAR>f : α → α<VAR>hf : Continuous f<GOAL>IsClosed (Function.fixedPoints f)
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>self : IntermediateField K L<VAR>x : L<GOAL>x ∈ self.carrier → x⁻¹ ∈ self.carrier
<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 : L<VAR>hx : x ∈ S<GOAL>-x ∈ S
<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 : L<GOAL>x ∈ s.carrier ↔ x ∈ s
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>S T : IntermediateField K L<VAR>h : ∀ (x : L), x ∈ S ↔ x ∈ T<GOAL>S = T
<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<GOAL>↑S.toSubalgebra = ↑S
<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<GOAL>↑S.toSubfield = ↑S
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>s : Subsemiring L<VAR>hK : ∀ (x : K), (algebraMap K L) x ∈ s<VAR>hi : ∀ x ∈ { toSubsemiring := s, algebraMap_mem' := hK }.carrier, x⁻¹ ∈ { toSubsemiring := s, algebraMap_mem' := hK }.carrier<VAR>x : L<GOAL>x ∈ { toSubsemiring := s, algebraMap_mem' := hK, inv_mem' := hi } ↔ x ∈ s
<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 : L<GOAL>x ∈ s.toSubalgebra ↔ x ∈ s
<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 : L<GOAL>x ∈ s.toSubfield ↔ x ∈ s
<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>s : Set L<VAR>hs : s = ↑S<GOAL>↑(S.copy s hs) = s
<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>s : Set L<VAR>hs : s = ↑S<GOAL>S.copy s hs = S
<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 : K<GOAL>(algebraMap K L) x ∈ S
<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>y : L<GOAL>y ∈ S → ∀ {x : K}, x • y ∈ S
<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<GOAL>1 ∈ S
<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<GOAL>0 ∈ S
<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 y : L<GOAL>x ∈ S → y ∈ S → x * y ∈ S
<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 y : L<GOAL>x ∈ S → y ∈ S → x + y ∈ S
<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 y : L<GOAL>x ∈ S → y ∈ S → x - y ∈ S
<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 : L<GOAL>x ∈ S → x⁻¹ ∈ S
<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 y : L<GOAL>x ∈ S → y ∈ S → x / y ∈ S
<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>l : List L<GOAL>(∀ x ∈ l, x ∈ S) → l.prod ∈ S
<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>l : List L<GOAL>(∀ x ∈ l, x ∈ S) → l.sum ∈ S
<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>m : Multiset L<GOAL>(∀ a ∈ m, a ∈ S) → m.prod ∈ S
<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>m : Multiset L<GOAL>(∀ a ∈ m, a ∈ S) → m.sum ∈ S
<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>ι : Type u_4<VAR>t : Finset ι<VAR>f : ι → L<VAR>h : ∀ c ∈ t, f c ∈ S<GOAL>∏ i ∈ t, f i ∈ S
<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>ι : Type u_4<VAR>t : Finset ι<VAR>f : ι → L<VAR>h : ∀ c ∈ t, f c ∈ S<GOAL>∑ i ∈ t, f i ∈ S
<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 : L<VAR>hx : x ∈ S<VAR>n : ℤ<GOAL>x ^ n ∈ S
<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 : L<VAR>hx : x ∈ S<VAR>n : ℤ<GOAL>n • x ∈ S
<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>n : ℤ<GOAL>↑n ∈ S
<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 y : ↥S<GOAL>↑(x + y) = ↑x + ↑y
<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>↑(-x) = -↑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 y : ↥S<GOAL>↑(x * y) = ↑x * ↑y
<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>↑x⁻¹ = (↑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<GOAL>↑0 = 0
<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<GOAL>↑1 = 1
<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<VAR>n : ℕ<GOAL>↑(x ^ n) = ↑x ^ n
<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>n : ℕ<GOAL>↑n ∈ S
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>S : Subalgebra K L<VAR>inv_mem : ∀ x ∈ S, x⁻¹ ∈ S<GOAL>(S.toIntermediateField inv_mem).toSubalgebra = S
<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<GOAL>S.toIntermediateField ⋯ = S
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>S : Subalgebra K L<VAR>hS : IsField ↥S<GOAL>(S.toIntermediateField' hS).toSubalgebra = S
<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<GOAL>S.toIntermediateField' ⋯ = S
<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>ι : Type u_4<VAR>Fintype ι<VAR>f : ι → ↥S<GOAL>↑(∑ i : ι, f i) = ∑ i : ι, ↑(f i)
<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>ι : Type u_4<VAR>Fintype ι<VAR>f : ι → ↥S<GOAL>↑(∏ i : ι, f i) = ∏ i : ι, ↑(f i)
<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>R : Type u_4<VAR>Semiring R<VAR>SMul R K<VAR>Module R L<VAR>IsScalarTower R K L<VAR>r : R<VAR>x : ↥S<GOAL>↑(r • x) = r • ↑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>(algebraMap (↥S) L) x = ↑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 : K<GOAL>↑((algebraMap K ↥S) x) = (algebraMap K L) x
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>L' : Type u_3<VAR>Field K<VAR>Field L<VAR>Field L'<VAR>Algebra K L<VAR>Algebra K L'<VAR>S : IntermediateField K L<VAR>f : L →ₐ[K] L'<GOAL>↑(IntermediateField.map f S) = ⇑f '' ↑S
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>L' : Type u_3<VAR>Field K<VAR>Field L<VAR>Field L'<VAR>Algebra K L<VAR>Algebra K L'<VAR>S : IntermediateField K L<VAR>f : L →ₐ[K] L'<GOAL>(IntermediateField.map f S).toSubalgebra = Subalgebra.map f S.toSubalgebra
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>L' : Type u_3<VAR>Field K<VAR>Field L<VAR>Field L'<VAR>Algebra K L<VAR>Algebra K L'<VAR>S : IntermediateField K L<VAR>f : L →ₐ[K] L'<GOAL>(IntermediateField.map f S).toSubfield = Subfield.map (↑f) S.toSubfield
<VAR>K : Type u_4<VAR>L₁ : Type u_5<VAR>L₂ : Type u_6<VAR>L₃ : Type u_7<VAR>Field K<VAR>Field L₁<VAR>Algebra K L₁<VAR>Field L₂<VAR>Algebra K L₂<VAR>Field L₃<VAR>Algebra K L₃<VAR>E : IntermediateField K L₁<VAR>f : L₁ →ₐ[K] L₂<VAR>g : L₂ →ₐ[K] L₃<GOAL>IntermediateField.map g (IntermediateField.map f E) = IntermediateField.map (g.comp f) E
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>L' : Type u_3<VAR>Field K<VAR>Field L<VAR>Field L'<VAR>Algebra K L<VAR>Algebra K L'<VAR>f : L →ₐ[K] L'<VAR>S T : IntermediateField K L<VAR>h : S ≤ T<GOAL>IntermediateField.map f S ≤ IntermediateField.map f T
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>L' : Type u_3<VAR>Field K<VAR>Field L<VAR>Field L'<VAR>Algebra K L<VAR>Algebra K L'<VAR>f : L →ₐ[K] L'<VAR>s : IntermediateField K L<VAR>t : IntermediateField K L'<GOAL>IntermediateField.map f s ≤ t ↔ s ≤ IntermediateField.comap f t
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>L' : Type u_3<VAR>Field K<VAR>Field L<VAR>Field L'<VAR>Algebra K L<VAR>Algebra K L'<VAR>f : L →ₐ[K] L'<GOAL>GaloisConnection (IntermediateField.map f) (IntermediateField.comap f)
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>L' : Type u_3<VAR>Field K<VAR>Field L<VAR>Field L'<VAR>Algebra K L<VAR>Algebra K L'<VAR>e : L ≃ₐ[K] L'<VAR>E : IntermediateField K L<VAR>a : ↥E<GOAL>↑((IntermediateField.intermediateFieldMap e E) a) = e ↑a
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>L' : Type u_3<VAR>Field K<VAR>Field L<VAR>Field L'<VAR>Algebra K L<VAR>Algebra K L'<VAR>e : L ≃ₐ[K] L'<VAR>E : IntermediateField K L<VAR>a : ↥(IntermediateField.map (↑e) E)<GOAL>↑((IntermediateField.intermediateFieldMap e E).symm a) = e.symm ↑a
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>L' : Type u_3<VAR>Field K<VAR>Field L<VAR>Field L'<VAR>Algebra K L<VAR>Algebra K L'<VAR>f : L →ₐ[K] L'<GOAL>f.fieldRange.toSubalgebra = f.range
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>L' : Type u_3<VAR>Field K<VAR>Field L<VAR>Field L'<VAR>Algebra K L<VAR>Algebra K L'<VAR>f : L →ₐ[K] L'<GOAL>↑f.fieldRange = Set.range ⇑f
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>L' : Type u_3<VAR>Field K<VAR>Field L<VAR>Field L'<VAR>Algebra K L<VAR>Algebra K L'<VAR>f : L →ₐ[K] L'<GOAL>f.fieldRange.toSubfield = (↑f).fieldRange
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>L' : Type u_3<VAR>Field K<VAR>Field L<VAR>Field L'<VAR>Algebra K L<VAR>Algebra K L'<VAR>f : L →ₐ[K] L'<VAR>y : L'<GOAL>y ∈ f.fieldRange ↔ ∃ x, f x = y
<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<GOAL>⇑S.val = Subtype.val
<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 : L<VAR>hx : x ∈ S<GOAL>S.val ⟨x, hx⟩ = 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<GOAL>S.val.range = S.toSubalgebra
<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<GOAL>S.val.fieldRange = S
<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>R : Type u_4<VAR>CommRing R<VAR>Algebra R K<VAR>Algebra R L<VAR>IsScalarTower R K L<VAR>x : ↥S<VAR>P : R[X]<GOAL>(Polynomial.aeval ↑x) P = ↑((Polynomial.aeval x) P)
<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>R : Type u_4<VAR>CommRing R<VAR>Algebra R K<VAR>Algebra R L<VAR>IsScalarTower R K L<VAR>x : ↥S<GOAL>IsIntegral R ↑x ↔ IsIntegral R x
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>E F : IntermediateField K L<VAR>hEF : E ≤ F<GOAL>Function.Injective ⇑(IntermediateField.inclusion hEF)
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>E : IntermediateField K L<GOAL>IntermediateField.inclusion ⋯ = AlgHom.id K ↥E
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>E F G : IntermediateField K L<VAR>hEF : E ≤ F<VAR>hFG : F ≤ G<VAR>x : ↥E<GOAL>(IntermediateField.inclusion hFG) ((IntermediateField.inclusion hEF) x) = (IntermediateField.inclusion ⋯) x
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>E F : IntermediateField K L<VAR>hEF : E ≤ F<VAR>e : ↥E<GOAL>↑((IntermediateField.inclusion hEF) e) = ↑e
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<GOAL>Function.Injective IntermediateField.toSubalgebra
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>L' : Type u_3<VAR>Field K<VAR>Field L<VAR>Field L'<VAR>Algebra K L<VAR>Algebra K L'<VAR>f : L →ₐ[K] L'<GOAL>Function.Injective (IntermediateField.map f)
<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<GOAL>Set.range ⇑(algebraMap K L) ⊆ ↑S
<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<GOAL>(algebraMap K L).fieldRange ≤ S.toSubfield
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>S S' : IntermediateField K L<GOAL>S.toSubalgebra ≤ S'.toSubalgebra ↔ S ≤ S'
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>S S' : IntermediateField K L<GOAL>S.toSubalgebra < S'.toSubalgebra ↔ S < S'
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>F : IntermediateField K L<GOAL>Function.Injective IntermediateField.lift
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>F : IntermediateField K L<VAR>E : IntermediateField K ↥F<GOAL>IntermediateField.lift E ≤ F
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>F : IntermediateField K L<VAR>E : IntermediateField K ↥F<VAR>x : ↥F<GOAL>↑x ∈ IntermediateField.lift E ↔ x ∈ E
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>L' : Type u_3<VAR>Field K<VAR>Field L<VAR>Field L'<VAR>Algebra K L<VAR>Algebra K L'<VAR>Algebra L' L<VAR>IsScalarTower K L' L<VAR>E : IntermediateField L' L<GOAL>↑(IntermediateField.restrictScalars K E) = ↑E
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>L' : Type u_3<VAR>Field K<VAR>Field L<VAR>Field L'<VAR>Algebra K L<VAR>Algebra K L'<VAR>Algebra L' L<VAR>IsScalarTower K L' L<VAR>E : IntermediateField L' L<GOAL>(IntermediateField.restrictScalars K E).toSubalgebra = Subalgebra.restrictScalars K E.toSubalgebra
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>L' : Type u_3<VAR>Field K<VAR>Field L<VAR>Field L'<VAR>Algebra K L<VAR>Algebra K L'<VAR>Algebra L' L<VAR>IsScalarTower K L' L<VAR>E : IntermediateField L' L<GOAL>(IntermediateField.restrictScalars K E).toSubfield = E.toSubfield
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>L' : Type u_3<VAR>Field K<VAR>Field L<VAR>Field L'<VAR>Algebra K L<VAR>Algebra K L'<VAR>Algebra L' L<VAR>IsScalarTower K L' L<VAR>E : IntermediateField L' L<VAR>x : L<GOAL>x ∈ IntermediateField.restrictScalars K E ↔ x ∈ E
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>L' : Type u_3<VAR>Field K<VAR>Field L<VAR>Field L'<VAR>Algebra K L<VAR>Algebra K L'<VAR>Algebra L' L<VAR>IsScalarTower K L' L<GOAL>Function.Injective (IntermediateField.restrictScalars K)
<VAR>L : Type u_2<VAR>Field L<VAR>F E : Subfield L<VAR>h : F ≤ E<GOAL>↑(Subfield.extendScalars h) = ↑E
<VAR>L : Type u_2<VAR>Field L<VAR>F E : Subfield L<VAR>h : F ≤ E<GOAL>(Subfield.extendScalars h).toSubfield = E
<VAR>L : Type u_2<VAR>Field L<VAR>F E : Subfield L<VAR>h : F ≤ E<VAR>x : L<GOAL>x ∈ Subfield.extendScalars h ↔ x ∈ E
<VAR>L : Type u_2<VAR>Field L<VAR>F E E' : Subfield L<VAR>h : F ≤ E<VAR>h' : F ≤ E'<GOAL>Subfield.extendScalars h ≤ Subfield.extendScalars h' ↔ E ≤ E'
<VAR>L : Type u_2<VAR>Field L<VAR>F E : Subfield L<VAR>h : F ≤ E<VAR>E' : IntermediateField (↥F) L<GOAL>Subfield.extendScalars h ≤ E' ↔ E ≤ E'.toSubfield
<VAR>L : Type u_2<VAR>Field L<VAR>F E : Subfield L<VAR>h : F ≤ E<VAR>E' : IntermediateField (↥F) L<GOAL>E' ≤ Subfield.extendScalars h ↔ E'.toSubfield ≤ E
<VAR>L : Type u_2<VAR>Field L<VAR>F : Subfield L<VAR>E : { E // F ≤ E }<GOAL>(Subfield.extendScalars.orderIso F) E = Subfield.extendScalars ⋯
<VAR>L : Type u_2<VAR>Field L<VAR>F : Subfield L<VAR>E : IntermediateField (↥F) L<GOAL>↑((RelIso.symm (Subfield.extendScalars.orderIso F)) E) = E.toSubfield
<VAR>L : Type u_2<VAR>Field L<VAR>F : Subfield L<GOAL>Function.Injective fun E => Subfield.extendScalars ⋯
<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>h : F ≤ E<GOAL>↑(IntermediateField.extendScalars h) = ↑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>h : F ≤ E<GOAL>(IntermediateField.extendScalars h).toSubfield = E.toSubfield
<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>h : F ≤ E<VAR>x : L<GOAL>x ∈ IntermediateField.extendScalars h ↔ x ∈ 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>h : F ≤ E<GOAL>IntermediateField.restrictScalars K (IntermediateField.extendScalars h) = E
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>F E E' : IntermediateField K L<VAR>h : F ≤ E<VAR>h' : F ≤ E'<GOAL>IntermediateField.extendScalars h ≤ IntermediateField.extendScalars h' ↔ E ≤ 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>h : F ≤ E<VAR>E' : IntermediateField (↥F) L<GOAL>IntermediateField.extendScalars h ≤ E' ↔ E ≤ IntermediateField.restrictScalars K 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>h : F ≤ E<VAR>E' : IntermediateField (↥F) L<GOAL>E' ≤ IntermediateField.extendScalars h ↔ IntermediateField.restrictScalars K E' ≤ E
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>F : IntermediateField K L<VAR>E : IntermediateField (↥F) L<GOAL>↑((RelIso.symm (IntermediateField.extendScalars.orderIso F)) E) = IntermediateField.restrictScalars K E
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>F : IntermediateField K L<VAR>E : { E // F ≤ E }<GOAL>(IntermediateField.extendScalars.orderIso F) E = IntermediateField.extendScalars ⋯
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>F : IntermediateField K L<GOAL>Function.Injective fun E => IntermediateField.extendScalars ⋯
<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>h : F ≤ E<VAR>x : ↥E<GOAL>x ∈ IntermediateField.restrict h ↔ ↑x ∈ F
<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>h : F ≤ E<GOAL>IntermediateField.lift (IntermediateField.restrict h) = F
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>F : IntermediateField K L<GOAL>Module.rank K ↥F.toSubalgebra = Module.rank K ↥F
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>F : IntermediateField K L<GOAL>FiniteDimensional.finrank K ↥F.toSubalgebra = FiniteDimensional.finrank K ↥F
<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<GOAL>F.toSubalgebra = E.toSubalgebra ↔ 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>hfin : FiniteDimensional K ↥E<VAR>h_le : F ≤ E<VAR>h_finrank : FiniteDimensional.finrank K ↥E ≤ FiniteDimensional.finrank K ↥F<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 K ↥E<VAR>h_le : F ≤ E<VAR>h_finrank : FiniteDimensional.finrank K ↥F = FiniteDimensional.finrank K ↥E<GOAL>F = E