ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type u_1<VAR>A : Type u_2<VAR>Field K<VAR>NumberField K<VAR>Field A<VAR>Algebra ℚ A<VAR>IsAlgClosed A<VAR>x : K<GOAL>(Set.range fun φ => φ x) = (minpoly ℚ x).rootSet A
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>A : Type u_2<VAR>NormedField A<VAR>IsAlgClosed A<VAR>NormedAlgebra ℚ A<VAR>B : ℝ<VAR>x : K<VAR>h : ∀ (φ : K →+* A), ‖φ x‖ ≤ B<VAR>i : ℕ<GOAL>‖(minpoly ℚ x).coeff i‖ ≤ max B 1 ^ FiniteDimensional.finrank ℚ K * ↑((FiniteDimensional.finrank ℚ K).choose (FiniteDimensional.finrank ℚ K / 2))
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>A : Type u_2<VAR>NormedField A<VAR>IsAlgClosed A<VAR>NormedAlgebra ℚ A<VAR>B : ℝ<GOAL>{x | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), ‖φ x‖ ≤ B}.Finite
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>A : Type u_2<VAR>NormedField A<VAR>IsAlgClosed A<VAR>NormedAlgebra ℚ A<VAR>x : K<VAR>hxi : IsIntegral ℤ x<VAR>hx : ∀ (φ : K →+* A), ‖φ x‖ = 1<GOAL>∃ n, ∃ (_ : 0 < n), x ^ n = 1
<VAR>K : Type u_1<VAR>Field K<VAR>A : Type u_2<VAR>NormedDivisionRing A<VAR>Nontrivial A<VAR>φ : K →+* A<VAR>x : K<GOAL>(NumberField.place φ) x = ‖φ x‖
<VAR>K : Type u_1<VAR>Field K<VAR>φ : K →+* ℂ<VAR>x : K<GOAL>(NumberField.ComplexEmbedding.conjugate φ) x = (starRingEnd ℂ) (φ x)
<VAR>K : Type u_1<VAR>Field K<VAR>φ : K →+* ℂ<GOAL>NumberField.place (NumberField.ComplexEmbedding.conjugate φ) = NumberField.place φ
<VAR>K : Type u_1<VAR>Field K<VAR>φ : K →+* ℂ<GOAL>NumberField.ComplexEmbedding.IsReal φ ↔ NumberField.ComplexEmbedding.conjugate φ = φ
<VAR>K : Type u_1<VAR>Field K<VAR>φ : K →+* ℂ<GOAL>NumberField.ComplexEmbedding.IsReal (NumberField.ComplexEmbedding.conjugate φ) ↔ NumberField.ComplexEmbedding.IsReal φ
<VAR>K : Type u_1<VAR>Field K<VAR>φ : K →+* ℂ<VAR>hφ : NumberField.ComplexEmbedding.IsReal φ<VAR>x : K<GOAL>↑(hφ.embedding x) = φ x
<VAR>K : Type u_1<VAR>Field K<VAR>k : Type u_2<VAR>Field k<VAR>f : k →+* K<VAR>φ : K →+* ℂ<VAR>hφ : NumberField.ComplexEmbedding.IsReal φ<GOAL>NumberField.ComplexEmbedding.IsReal (φ.comp f)
<VAR>K : Type u_1<VAR>Field K<VAR>k : Type u_2<VAR>Field k<VAR>f : k ≃+* K<VAR>φ : K →+* ℂ<GOAL>NumberField.ComplexEmbedding.IsReal (φ.comp ↑f) ↔ NumberField.ComplexEmbedding.IsReal φ
<VAR>K : Type u_1<VAR>Field K<VAR>k : Type u_2<VAR>Field k<VAR>Algebra k K<VAR>IsGalois k K<VAR>φ ψ : K →+* ℂ<VAR>h : φ.comp (algebraMap k K) = ψ.comp (algebraMap k K)<GOAL>∃ σ, φ.comp ↑σ.symm = ψ
<VAR>K : Type u_1<VAR>Field K<VAR>k : Type u_2<VAR>Field k<VAR>Algebra k K<VAR>φ : K →+* ℂ<VAR>σ : K ≃ₐ[k] K<VAR>h : NumberField.ComplexEmbedding.IsConj φ σ<VAR>x : K<GOAL>φ (σ x) = star (φ x)
<VAR>K : Type u_1<VAR>Field K<VAR>k : Type u_2<VAR>Field k<VAR>Algebra k K<VAR>φ : K →+* ℂ<VAR>σ₁ σ₂ : K ≃ₐ[k] K<VAR>h₁ : NumberField.ComplexEmbedding.IsConj φ σ₁<VAR>h₂ : NumberField.ComplexEmbedding.IsConj φ σ₂<GOAL>σ₁ = σ₂
<VAR>K : Type u_1<VAR>Field K<VAR>k : Type u_2<VAR>Field k<VAR>Algebra k K<VAR>φ : K →+* ℂ<VAR>σ₁ σ₂ : K ≃ₐ[k] K<VAR>h₁ : NumberField.ComplexEmbedding.IsConj φ σ₁<GOAL>σ₁ = σ₂ ↔ NumberField.ComplexEmbedding.IsConj φ σ₂
<VAR>K : Type u_1<VAR>Field K<VAR>k : Type u_2<VAR>Field k<VAR>Algebra k K<VAR>φ : K →+* ℂ<VAR>σ : K ≃ₐ[k] K<VAR>h : NumberField.ComplexEmbedding.IsConj φ σ<GOAL>NumberField.ComplexEmbedding.IsReal (φ.comp (algebraMap k K))
<VAR>K : Type u_1<VAR>Field K<VAR>k : Type u_2<VAR>Field k<VAR>Algebra k K<VAR>φ : K →+* ℂ<GOAL>NumberField.ComplexEmbedding.IsConj φ 1 ↔ NumberField.ComplexEmbedding.IsReal φ
<VAR>K : Type u_1<VAR>Field K<VAR>k : Type u_2<VAR>Field k<VAR>Algebra k K<VAR>φ : K →+* ℂ<VAR>σ : K ≃ₐ[k] K<VAR>hσ : NumberField.ComplexEmbedding.IsConj φ σ<GOAL>NumberField.ComplexEmbedding.IsConj φ σ.symm
<VAR>K : Type u_1<VAR>Field K<VAR>k : Type u_2<VAR>Field k<VAR>Algebra k K<VAR>φ : K →+* ℂ<VAR>σ : K ≃ₐ[k] K<GOAL>NumberField.ComplexEmbedding.IsConj φ σ.symm ↔ NumberField.ComplexEmbedding.IsConj φ σ
<VAR>K : Type u_2<VAR>Field K<VAR>φ : K →+* ℂ<VAR>x : K<GOAL>(NumberField.InfinitePlace.mk φ) x = Complex.abs (φ x)
<VAR>K : Type u_2<VAR>Field K<VAR>w : NumberField.InfinitePlace K<GOAL>NumberField.InfinitePlace.mk w.embedding = w
<VAR>K : Type u_2<VAR>Field K<VAR>φ : K →+* ℂ<GOAL>NumberField.InfinitePlace.mk (NumberField.ComplexEmbedding.conjugate φ) = NumberField.InfinitePlace.mk φ
<VAR>K : Type u_2<VAR>Field K<VAR>w : NumberField.InfinitePlace K<VAR>x : K<GOAL>‖w.embedding x‖ = w x
<VAR>K : Type u_2<VAR>Field K<VAR>x : K<VAR>r : ℝ<GOAL>(∀ (w : NumberField.InfinitePlace K), w x = r) ↔ ∀ (φ : K →+* ℂ), ‖φ x‖ = r
<VAR>K : Type u_2<VAR>Field K<VAR>x : K<VAR>r : ℝ<GOAL>(∀ (w : NumberField.InfinitePlace K), w x ≤ r) ↔ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r
<VAR>K : Type u_2<VAR>Field K<VAR>w : NumberField.InfinitePlace K<VAR>x : K<GOAL>0 < w x ↔ x ≠ 0
<VAR>K : Type u_2<VAR>Field K<VAR>φ ψ : K →+* ℂ<GOAL>NumberField.InfinitePlace.mk φ = NumberField.InfinitePlace.mk ψ ↔ φ = ψ ∨ NumberField.ComplexEmbedding.conjugate φ = ψ
<VAR>K : Type u_2<VAR>Field K<VAR>φ : K →+* ℂ<GOAL>(NumberField.InfinitePlace.mk φ).embedding = φ ∨ (NumberField.InfinitePlace.mk φ).embedding = NumberField.ComplexEmbedding.conjugate φ
<VAR>K : Type u_2<VAR>Field K<VAR>φ : K →+* ℂ<VAR>h : NumberField.ComplexEmbedding.IsReal φ<GOAL>(NumberField.InfinitePlace.mk φ).embedding = φ
<VAR>K : Type u_2<VAR>Field K<VAR>w : NumberField.InfinitePlace K<GOAL>w.IsReal ↔ NumberField.ComplexEmbedding.IsReal w.embedding
<VAR>K : Type u_2<VAR>Field K<VAR>w : NumberField.InfinitePlace K<GOAL>w.IsComplex ↔ ¬NumberField.ComplexEmbedding.IsReal w.embedding
<VAR>K : Type u_2<VAR>Field K<VAR>w : NumberField.InfinitePlace K<VAR>h : w.IsReal<GOAL>NumberField.ComplexEmbedding.conjugate w.embedding = w.embedding
<VAR>K : Type u_2<VAR>Field K<VAR>w : NumberField.InfinitePlace K<GOAL>¬w.IsReal ↔ w.IsComplex
<VAR>K : Type u_2<VAR>Field K<VAR>w : NumberField.InfinitePlace K<GOAL>¬w.IsComplex ↔ w.IsReal
<VAR>K : Type u_2<VAR>Field K<VAR>w : NumberField.InfinitePlace K<GOAL>w.IsReal ∨ w.IsComplex
<VAR>K : Type u_2<VAR>Field K<VAR>w w' : NumberField.InfinitePlace K<VAR>h : w.IsReal<VAR>h' : w'.IsComplex<GOAL>w ≠ w'
<VAR>K : Type u_2<VAR>Field K<GOAL>Disjoint {w | w.IsReal} {w | w.IsComplex}
<VAR>K : Type u_2<VAR>Field K<VAR>w : NumberField.InfinitePlace K<VAR>hw : w.IsReal<VAR>x : K<GOAL>↑((NumberField.InfinitePlace.embedding_of_isReal hw) x) = w.embedding x
<VAR>K : Type u_2<VAR>Field K<VAR>w : NumberField.InfinitePlace K<VAR>hw : w.IsReal<VAR>x : K<GOAL>‖(NumberField.InfinitePlace.embedding_of_isReal hw) x‖ = w x
<VAR>K : Type u_2<VAR>Field K<VAR>φ : K →+* ℂ<VAR>h : (NumberField.InfinitePlace.mk φ).IsReal<GOAL>NumberField.ComplexEmbedding.IsReal φ
<VAR>K : Type u_2<VAR>Field K<VAR>φ : K →+* ℂ<GOAL>(NumberField.InfinitePlace.mk φ).IsReal ↔ NumberField.ComplexEmbedding.IsReal φ
<VAR>K : Type u_2<VAR>Field K<VAR>φ : K →+* ℂ<GOAL>(NumberField.InfinitePlace.mk φ).IsComplex ↔ ¬NumberField.ComplexEmbedding.IsReal φ
<VAR>K : Type u_2<VAR>Field K<VAR>φ : K →+* ℂ<VAR>h : (NumberField.InfinitePlace.mk φ).IsComplex<GOAL>¬NumberField.ComplexEmbedding.IsReal φ
<VAR>K : Type u_2<VAR>Field K<VAR>w : NumberField.InfinitePlace K<GOAL>0 < w.mult
<VAR>K : Type u_2<VAR>Field K<VAR>w : NumberField.InfinitePlace K<GOAL>w.mult ≠ 0
<VAR>K : Type u_2<VAR>Field K<VAR>w : NumberField.InfinitePlace K<GOAL>1 ≤ ↑w.mult
<VAR>K : Type u_2<VAR>Field K<VAR>NumberField K<VAR>w : NumberField.InfinitePlace K<GOAL>(Finset.filter (fun φ => NumberField.InfinitePlace.mk φ = w) Finset.univ).card = w.mult
<VAR>K : Type u_2<VAR>Field K<VAR>NumberField K<GOAL>∑ w : NumberField.InfinitePlace K, w.mult = FiniteDimensional.finrank ℚ K
<VAR>K : Type u_2<VAR>Field K<VAR>φ : { φ // NumberField.ComplexEmbedding.IsReal φ }<GOAL>↑(NumberField.InfinitePlace.mkReal φ) = NumberField.InfinitePlace.mk ↑φ
<VAR>K : Type u_2<VAR>Field K<VAR>φ : { φ // ¬NumberField.ComplexEmbedding.IsReal φ }<GOAL>↑(NumberField.InfinitePlace.mkComplex φ) = NumberField.InfinitePlace.mk ↑φ
<VAR>K : Type u_2<VAR>Field K<VAR>NumberField K<VAR>x : K<GOAL>∏ w : NumberField.InfinitePlace K, w x ^ w.mult = ↑|(Algebra.norm ℚ) x|
<VAR>K : Type u_2<VAR>Field K<VAR>NumberField K<VAR>w : NumberField.InfinitePlace K<VAR>a : NumberField.RingOfIntegers K<VAR>ha : a ≠ 0<VAR>h : ∀ ⦃z : NumberField.InfinitePlace K⦄, z ≠ w → z ↑a < 1<GOAL>1 ≤ w ↑a
<VAR>K : Type u_2<VAR>Field K<VAR>NumberField K<VAR>x : NumberField.RingOfIntegers K<VAR>w : NumberField.InfinitePlace K<VAR>h₁ : x ≠ 0<VAR>h₂ : ∀ ⦃w' : NumberField.InfinitePlace K⦄, w' ≠ w → w' ↑x < 1<VAR>h₃ : w.IsReal ∨ |(w.embedding ↑x).re| < 1<GOAL>ℚ⟮↑x⟯ = ⊤
<VAR>K : Type u_2<VAR>Field K<VAR>NumberField K<VAR>x : NumberField.RingOfIntegers K<VAR>w : NumberField.InfinitePlace K<VAR>h₁ : x ≠ 0<VAR>h₂ : ∀ ⦃w' : NumberField.InfinitePlace K⦄, w' ≠ w → w' ↑x < 1<VAR>h₃ : w.IsReal ∨ |(w.embedding ↑x).re| < 1<GOAL>Algebra.adjoin ℚ {↑x} = ⊤
<VAR>K : Type u_2<VAR>Field K<VAR>NumberField K<GOAL>Fintype.card { φ // NumberField.ComplexEmbedding.IsReal φ } = NumberField.InfinitePlace.NrRealPlaces K
<VAR>K : Type u_2<VAR>Field K<VAR>NumberField K<GOAL>Fintype.card (NumberField.InfinitePlace K) = NumberField.InfinitePlace.NrRealPlaces K + NumberField.InfinitePlace.NrComplexPlaces K
<VAR>K : Type u_2<VAR>Field K<VAR>NumberField K<GOAL>Fintype.card { φ // ¬NumberField.ComplexEmbedding.IsReal φ } = 2 * NumberField.InfinitePlace.NrComplexPlaces K
<VAR>K : Type u_2<VAR>Field K<VAR>NumberField K<GOAL>NumberField.InfinitePlace.NrRealPlaces K + 2 * NumberField.InfinitePlace.NrComplexPlaces K = FiniteDimensional.finrank ℚ K
<VAR>K : Type u_2<VAR>Field K<VAR>NumberField K<VAR>h : FiniteDimensional.finrank ℚ K = 1<GOAL>NumberField.InfinitePlace.NrComplexPlaces K = 0
<VAR>K : Type u_2<VAR>Field K<VAR>NumberField K<VAR>h : FiniteDimensional.finrank ℚ K = 1<GOAL>NumberField.InfinitePlace.NrRealPlaces K = 1
<VAR>k : Type u_1<VAR>Field k<VAR>K : Type u_2<VAR>Field K<VAR>φ : K →+* ℂ<VAR>f : k →+* K<GOAL>(NumberField.InfinitePlace.mk φ).comap f = NumberField.InfinitePlace.mk (φ.comp f)
<VAR>K : Type u_2<VAR>Field K<VAR>w : NumberField.InfinitePlace K<GOAL>w.comap (RingHom.id K) = w
<VAR>k : Type u_1<VAR>Field k<VAR>K : Type u_2<VAR>Field K<VAR>F : Type u_3<VAR>Field F<VAR>w : NumberField.InfinitePlace K<VAR>f : F →+* K<VAR>g : k →+* F<GOAL>w.comap (f.comp g) = (w.comap f).comap g
<VAR>k : Type u_1<VAR>Field k<VAR>K : Type u_2<VAR>Field K<VAR>f : k →+* K<VAR>w : NumberField.InfinitePlace K<VAR>hφ : w.IsReal<GOAL>(w.comap f).IsReal
<VAR>k : Type u_1<VAR>Field k<VAR>K : Type u_2<VAR>Field K<VAR>f : k ≃+* K<VAR>w : NumberField.InfinitePlace K<GOAL>(w.comap ↑f).IsReal ↔ w.IsReal
<VAR>k : Type u_1<VAR>Field k<VAR>K : Type u_2<VAR>Field K<VAR>Algebra k K<VAR>Algebra.IsAlgebraic k K<GOAL>Function.Surjective fun x => x.comap (algebraMap k K)
<VAR>k : Type u_1<VAR>Field k<VAR>K : Type u_2<VAR>Field K<VAR>f : k →+* K<VAR>w : NumberField.InfinitePlace K<GOAL>(w.comap f).mult ≤ w.mult
<VAR>k : Type u_1<VAR>Field k<VAR>K : Type u_2<VAR>Field K<VAR>Algebra k K<VAR>NumberField k<VAR>NumberField K<GOAL>Fintype.card (NumberField.InfinitePlace k) ≤ Fintype.card (NumberField.InfinitePlace K)
<VAR>k : Type u_1<VAR>Field k<VAR>K : Type u_2<VAR>Field K<VAR>Algebra k K<VAR>σ : K ≃ₐ[k] K<VAR>w : NumberField.InfinitePlace K<GOAL>∀ (a : K), ↑(SMul.smul σ w) a = ↑w (σ.symm a)
<VAR>k : Type u_1<VAR>Field k<VAR>K : Type u_2<VAR>Field K<VAR>Algebra k K<VAR>σ : K ≃ₐ[k] K<VAR>w : NumberField.InfinitePlace K<GOAL>σ • w = w.comap ↑σ.symm
<VAR>k : Type u_1<VAR>Field k<VAR>K : Type u_2<VAR>Field K<VAR>Algebra k K<VAR>σ : K ≃ₐ[k] K<VAR>w : NumberField.InfinitePlace K<VAR>x : K<GOAL>(σ • w) x = w (σ.symm x)
<VAR>k : Type u_1<VAR>Field k<VAR>K : Type u_2<VAR>Field K<VAR>Algebra k K<VAR>σ : K ≃ₐ[k] K<VAR>φ : K →+* ℂ<GOAL>σ • NumberField.InfinitePlace.mk φ = NumberField.InfinitePlace.mk (φ.comp ↑σ.symm)
<VAR>k : Type u_1<VAR>Field k<VAR>K : Type u_2<VAR>Field K<VAR>F : Type u_3<VAR>Field F<VAR>Algebra k K<VAR>σ : K ≃ₐ[k] K<VAR>w : NumberField.InfinitePlace K<VAR>f : F →+* K<GOAL>(σ • w).comap f = w.comap ((↑σ.symm).comp f)
<VAR>k : Type u_1<VAR>Field k<VAR>K : Type u_2<VAR>Field K<VAR>Algebra k K<VAR>σ : K ≃ₐ[k] K<VAR>w : NumberField.InfinitePlace K<GOAL>(σ • w).IsReal ↔ w.IsReal
<VAR>k : Type u_1<VAR>Field k<VAR>K : Type u_2<VAR>Field K<VAR>Algebra k K<VAR>σ : K ≃ₐ[k] K<VAR>w : NumberField.InfinitePlace K<GOAL>(σ • w).IsComplex ↔ w.IsComplex
<VAR>k : Type u_1<VAR>Field k<VAR>K : Type u_2<VAR>Field K<VAR>Algebra k K<VAR>IsGalois k K<VAR>φ ψ : K →+* ℂ<VAR>h : φ.comp (algebraMap k K) = ψ.comp (algebraMap k K)<GOAL>∃ σ, φ.comp ↑σ.symm = ψ
<VAR>k : Type u_1<VAR>Field k<VAR>K : Type u_2<VAR>Field K<VAR>Algebra k K<VAR>IsGalois k K<VAR>w w' : NumberField.InfinitePlace K<VAR>h : w.comap (algebraMap k K) = w'.comap (algebraMap k K)<GOAL>∃ σ, σ • w = w'
<VAR>k : Type u_1<VAR>Field k<VAR>K : Type u_2<VAR>Field K<VAR>Algebra k K<VAR>IsGalois k K<VAR>w w' : NumberField.InfinitePlace K<GOAL>w' ∈ MulAction.orbit (K ≃ₐ[k] K) w ↔ w.comap (algebraMap k K) = w'.comap (algebraMap k K)
<VAR>k : Type u_1<VAR>Field k<VAR>K : Type u_2<VAR>Field K<VAR>Algebra k K<VAR>IsGalois k K<VAR>w : NumberField.InfinitePlace K<GOAL>NumberField.InfinitePlace.orbitRelEquiv (Quotient.mk'' w) = w.comap (algebraMap k K)
<VAR>K : Type u_2<VAR>Field K<VAR>w : NumberField.InfinitePlace K<GOAL>NumberField.InfinitePlace.IsUnramified K w
<VAR>k : Type u_1<VAR>Field k<VAR>K : Type u_2<VAR>Field K<VAR>Algebra k K<VAR>w : NumberField.InfinitePlace K<VAR>h : NumberField.InfinitePlace.IsUnramified k w<GOAL>(w.comap (algebraMap k K)).mult = w.mult
<VAR>k : Type u_1<VAR>Field k<VAR>K : Type u_2<VAR>Field K<VAR>Algebra k K<VAR>w : NumberField.InfinitePlace K<GOAL>NumberField.InfinitePlace.IsUnramified k w ↔ w.mult ≤ (w.comap (algebraMap k K)).mult
<VAR>k : Type u_1<VAR>Field k<VAR>K : Type u_2<VAR>Field K<VAR>F : Type u_3<VAR>Field F<VAR>Algebra k K<VAR>Algebra k F<VAR>w : NumberField.InfinitePlace F<VAR>h : NumberField.InfinitePlace.IsUnramified k w<VAR>f : K →ₐ[k] F<GOAL>NumberField.InfinitePlace.IsUnramified k (w.comap ↑f)
<VAR>k : Type u_1<VAR>Field k<VAR>K : Type u_2<VAR>Field K<VAR>F : Type u_3<VAR>Field F<VAR>Algebra k K<VAR>Algebra k F<VAR>Algebra K F<VAR>IsScalarTower k K F<VAR>w : NumberField.InfinitePlace F<VAR>h : NumberField.InfinitePlace.IsUnramified k w<GOAL>NumberField.InfinitePlace.IsUnramified K w
<VAR>k : Type u_1<VAR>Field k<VAR>K : Type u_2<VAR>Field K<VAR>F : Type u_3<VAR>Field F<VAR>Algebra k K<VAR>Algebra k F<VAR>Algebra K F<VAR>IsScalarTower k K F<VAR>w : NumberField.InfinitePlace F<VAR>h : NumberField.InfinitePlace.IsUnramified k w<GOAL>NumberField.InfinitePlace.IsUnramified k (w.comap (algebraMap K F))
<VAR>k : Type u_1<VAR>Field k<VAR>K : Type u_2<VAR>Field K<VAR>Algebra k K<VAR>w : NumberField.InfinitePlace K<GOAL>¬NumberField.InfinitePlace.IsUnramified k w ↔ w.IsComplex ∧ (w.comap (algebraMap k K)).IsReal
<VAR>k : Type u_1<VAR>Field k<VAR>K : Type u_2<VAR>Field K<VAR>Algebra k K<VAR>w : NumberField.InfinitePlace K<GOAL>NumberField.InfinitePlace.IsUnramified k w ↔ w.IsReal ∨ (w.comap (algebraMap k K)).IsComplex
<VAR>k : Type u_1<VAR>Field k<VAR>K : Type u_2<VAR>Field K<VAR>Algebra k K<VAR>w : NumberField.InfinitePlace K<VAR>h : w.IsReal<GOAL>NumberField.InfinitePlace.IsUnramified k w
<VAR>k : Type u_1<VAR>Field k<VAR>K : Type u_2<VAR>Field K<VAR>Algebra k K<VAR>σ : K ≃ₐ[k] K<VAR>φ : K →+* ℂ<VAR>h : NumberField.ComplexEmbedding.IsConj φ σ<GOAL>NumberField.InfinitePlace.IsUnramified k (NumberField.InfinitePlace.mk φ) ↔ σ = 1
<VAR>k : Type u_1<VAR>Field k<VAR>K : Type u_2<VAR>Field K<VAR>Algebra k K<VAR>IsGalois k K<VAR>φ : K →+* ℂ<GOAL>NumberField.InfinitePlace.IsUnramified k (NumberField.InfinitePlace.mk φ) ↔ ∀ (σ : K ≃ₐ[k] K), NumberField.ComplexEmbedding.IsConj φ σ → σ = 1
<VAR>k : Type u_1<VAR>Field k<VAR>K : Type u_2<VAR>Field K<VAR>Algebra k K<VAR>φ : K →+* ℂ<VAR>σ : K ≃ₐ[k] K<GOAL>σ ∈ MulAction.stabilizer (K ≃ₐ[k] K) (NumberField.InfinitePlace.mk φ) ↔ σ = 1 ∨ NumberField.ComplexEmbedding.IsConj φ σ
<VAR>k : Type u_1<VAR>Field k<VAR>K : Type u_2<VAR>Field K<VAR>Algebra k K<VAR>w : NumberField.InfinitePlace K<VAR>h : NumberField.InfinitePlace.IsUnramified k w<GOAL>MulAction.stabilizer (K ≃ₐ[k] K) w = ⊥
<VAR>k : Type u_1<VAR>Field k<VAR>K : Type u_2<VAR>Field K<VAR>Algebra k K<VAR>σ : K ≃ₐ[k] K<VAR>φ : K →+* ℂ<VAR>h : NumberField.ComplexEmbedding.IsConj φ σ<GOAL>↑(MulAction.stabilizer (K ≃ₐ[k] K) (NumberField.InfinitePlace.mk φ)) = {1, σ}
<VAR>k : Type u_1<VAR>Field k<VAR>K : Type u_2<VAR>Field K<VAR>Algebra k K<VAR>w : NumberField.InfinitePlace K<GOAL>Nat.card ↥(MulAction.stabilizer (K ≃ₐ[k] K) w) = 1 ∨ Nat.card ↥(MulAction.stabilizer (K ≃ₐ[k] K) w) = 2
<VAR>k : Type u_1<VAR>Field k<VAR>K : Type u_2<VAR>Field K<VAR>Algebra k K<VAR>w : NumberField.InfinitePlace K<VAR>IsGalois k K<GOAL>NumberField.InfinitePlace.IsUnramified k w ↔ MulAction.stabilizer (K ≃ₐ[k] K) w = ⊥
<VAR>k : Type u_1<VAR>Field k<VAR>K : Type u_2<VAR>Field K<VAR>Algebra k K<VAR>w : NumberField.InfinitePlace K<VAR>IsGalois k K<GOAL>NumberField.InfinitePlace.IsUnramified k w ↔ Nat.card ↥(MulAction.stabilizer (K ≃ₐ[k] K) w) = 1
<VAR>k : Type u_1<VAR>Field k<VAR>K : Type u_2<VAR>Field K<VAR>Algebra k K<VAR>w : NumberField.InfinitePlace K<VAR>IsGalois k K<GOAL>¬NumberField.InfinitePlace.IsUnramified k w ↔ Nat.card ↥(MulAction.stabilizer (K ≃ₐ[k] K) w) = 2
<VAR>k : Type u_1<VAR>Field k<VAR>K : Type u_2<VAR>Field K<VAR>Algebra k K<VAR>w : NumberField.InfinitePlace K<VAR>IsGalois k K<GOAL>Nat.card ↥(MulAction.stabilizer (K ≃ₐ[k] K) w) = if NumberField.InfinitePlace.IsUnramified k w then 1 else 2
<VAR>k : Type u_1<VAR>Field k<VAR>K : Type u_2<VAR>Field K<VAR>Algebra k K<VAR>w : NumberField.InfinitePlace K<VAR>IsGalois k K<VAR>hw : ¬NumberField.InfinitePlace.IsUnramified k w<GOAL>Even (Nat.card (K ≃ₐ[k] K))
<VAR>k : Type u_1<VAR>Field k<VAR>K : Type u_2<VAR>Field K<VAR>Algebra k K<VAR>w : NumberField.InfinitePlace K<VAR>IsGalois k K<VAR>FiniteDimensional k K<VAR>hw : ¬NumberField.InfinitePlace.IsUnramified k w<GOAL>Even (Fintype.card (K ≃ₐ[k] K))
<VAR>k : Type u_1<VAR>Field k<VAR>K : Type u_2<VAR>Field K<VAR>Algebra k K<VAR>w : NumberField.InfinitePlace K<VAR>IsGalois k K<VAR>hw : ¬NumberField.InfinitePlace.IsUnramified k w<GOAL>Even (FiniteDimensional.finrank k K)
<VAR>k : Type u_1<VAR>Field k<VAR>K : Type u_2<VAR>Field K<VAR>Algebra k K<VAR>σ : K ≃ₐ[k] K<VAR>w : NumberField.InfinitePlace K<GOAL>NumberField.InfinitePlace.IsUnramified k (σ • w) ↔ NumberField.InfinitePlace.IsUnramified k w
<VAR>k : Type u_1<VAR>Field k<VAR>K : Type u_2<VAR>Field K<VAR>Algebra k K<VAR>IsGalois k K<VAR>w : NumberField.InfinitePlace K<GOAL>NumberField.InfinitePlace.IsUnramifiedIn K (w.comap (algebraMap k K)) ↔ NumberField.InfinitePlace.IsUnramified k w
<VAR>k : Type u_1<VAR>Field k<VAR>K : Type u_2<VAR>Field K<VAR>Algebra k K<VAR>IsGalois k K<VAR>FiniteDimensional k K<VAR>w : NumberField.InfinitePlace k<VAR>hw : ¬NumberField.InfinitePlace.IsUnramifiedIn K w<GOAL>Even (Fintype.card (K ≃ₐ[k] K))
<VAR>k : Type u_1<VAR>Field k<VAR>K : Type u_2<VAR>Field K<VAR>Algebra k K<VAR>IsGalois k K<VAR>w : NumberField.InfinitePlace k<VAR>hw : ¬NumberField.InfinitePlace.IsUnramifiedIn K w<GOAL>Even (FiniteDimensional.finrank k K)
<VAR>k : Type u_1<VAR>Field k<VAR>K : Type u_2<VAR>Field K<VAR>NumberField K<VAR>Algebra k K<VAR>NumberField k<VAR>IsGalois k K<GOAL>(Finset.filter (NumberField.InfinitePlace.IsUnramified k) Finset.univ).card = (Finset.filter (NumberField.InfinitePlace.IsUnramifiedIn K) Finset.univ).card * FiniteDimensional.finrank k K
<VAR>k : Type u_1<VAR>Field k<VAR>K : Type u_2<VAR>Field K<VAR>NumberField K<VAR>Algebra k K<VAR>NumberField k<VAR>IsGalois k K<GOAL>(Finset.filter (NumberField.InfinitePlace.IsUnramified k) Finset.univ)ᶜ.card = (Finset.filter (NumberField.InfinitePlace.IsUnramifiedIn K) Finset.univ)ᶜ.card * (FiniteDimensional.finrank k K / 2)
<VAR>k : Type u_1<VAR>Field k<VAR>K : Type u_2<VAR>Field K<VAR>NumberField K<VAR>Algebra k K<VAR>NumberField k<VAR>IsGalois k K<GOAL>Fintype.card (NumberField.InfinitePlace K) = (Finset.filter (NumberField.InfinitePlace.IsUnramifiedIn K) Finset.univ).card * FiniteDimensional.finrank k K + (Finset.filter (NumberField.InfinitePlace.IsUnramifiedIn K) Finset.univ)ᶜ.card * (FiniteDimensional.finrank k K / 2)
<VAR>k : Type u_1<VAR>Field k<VAR>K : Type u_2<VAR>Field K<VAR>Algebra k K<VAR>self : IsUnramifiedAtInfinitePlaces k K<VAR>w : NumberField.InfinitePlace K<GOAL>NumberField.InfinitePlace.IsUnramified k w
<VAR>k : Type u_1<VAR>Field k<VAR>K : Type u_2<VAR>Field K<VAR>F : Type u_3<VAR>Field F<VAR>Algebra k K<VAR>Algebra k F<VAR>Algebra K F<VAR>IsScalarTower k K F<VAR>h₁ : IsUnramifiedAtInfinitePlaces k K<VAR>h₂ : IsUnramifiedAtInfinitePlaces K F<GOAL>IsUnramifiedAtInfinitePlaces k F
<VAR>k : Type u_1<VAR>Field k<VAR>K : Type u_2<VAR>Field K<VAR>F : Type u_3<VAR>Field F<VAR>Algebra k K<VAR>Algebra k F<VAR>Algebra K F<VAR>IsScalarTower k K F<VAR>h : IsUnramifiedAtInfinitePlaces k F<GOAL>IsUnramifiedAtInfinitePlaces K F
<VAR>k : Type u_1<VAR>Field k<VAR>K : Type u_2<VAR>Field K<VAR>F : Type u_3<VAR>Field F<VAR>Algebra k K<VAR>Algebra k F<VAR>Algebra K F<VAR>IsScalarTower k K F<VAR>h₁ : IsUnramifiedAtInfinitePlaces k F<VAR>Algebra.IsAlgebraic K F<GOAL>IsUnramifiedAtInfinitePlaces k K
<VAR>k : Type u_1<VAR>Field k<VAR>K : Type u_2<VAR>Field K<VAR>Algebra k K<VAR>IsUnramifiedAtInfinitePlaces k K<VAR>w : NumberField.InfinitePlace K<GOAL>NumberField.InfinitePlace.IsUnramified k w
<VAR>k : Type u_1<VAR>Field k<VAR>K : Type u_2<VAR>Field K<VAR>Algebra k K<VAR>IsUnramifiedAtInfinitePlaces k K<VAR>w : NumberField.InfinitePlace k<GOAL>NumberField.InfinitePlace.IsUnramifiedIn K w
<VAR>k : Type u_1<VAR>Field k<VAR>K : Type u_2<VAR>Field K<VAR>Algebra k K<VAR>IsGalois k K<VAR>FiniteDimensional k K<VAR>h : Odd (Fintype.card (K ≃ₐ[k] K))<GOAL>IsUnramifiedAtInfinitePlaces k K
<VAR>k : Type u_1<VAR>Field k<VAR>K : Type u_2<VAR>Field K<VAR>Algebra k K<VAR>IsGalois k K<VAR>h : Odd (FiniteDimensional.finrank k K)<GOAL>IsUnramifiedAtInfinitePlaces k K
<VAR>k : Type u_1<VAR>Field k<VAR>K : Type u_2<VAR>Field K<VAR>Algebra k K<VAR>NumberField k<VAR>NumberField K<VAR>IsGalois k K<VAR>IsUnramifiedAtInfinitePlaces k K<GOAL>Fintype.card (NumberField.InfinitePlace K) = Fintype.card (NumberField.InfinitePlace k) * FiniteDimensional.finrank k K
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>ζ : K<VAR>k : ℕ<VAR>hk : 2 < k<VAR>hζ : IsPrimitiveRoot ζ k<GOAL>NumberField.InfinitePlace.NrRealPlaces K = 0
<VAR>n : ℕ+<VAR>K : Type u<VAR>Field K<VAR>CharZero K<VAR>IsCyclotomicExtension {n} ℚ K<VAR>hn : 2 < n<GOAL>NumberField.InfinitePlace.NrRealPlaces K = 0
<VAR>n : ℕ+<VAR>K : Type u<VAR>Field K<VAR>CharZero K<VAR>h : IsCyclotomicExtension {n} ℚ K<GOAL>NumberField.InfinitePlace.NrComplexPlaces K = (↑n).totient / 2
<VAR>n : ℕ+<VAR>K : Type u_1<VAR>Field K<VAR>L : Type u_2<VAR>μ : L<VAR>CommRing L<VAR>IsDomain L<VAR>hμ : IsPrimitiveRoot μ ↑n<VAR>Algebra K L<VAR>IsCyclotomicExtension {n} K L<GOAL>Function.Injective ⇑(IsPrimitiveRoot.autToPow K hμ)
<VAR>n : ℕ+<VAR>K : Type u_1<VAR>Field K<VAR>L : Type u_2<VAR>CommRing L<VAR>IsDomain L<VAR>Algebra K L<VAR>IsCyclotomicExtension {n} K L<VAR>h : Irreducible (Polynomial.cyclotomic (↑n) K)<GOAL>∀ (a : L ≃ₐ[K] L), (IsCyclotomicExtension.autEquivPow L h) a = (↑(IsPrimitiveRoot.autToPow K ⋯)).toFun a
<VAR>n : ℕ+<VAR>K : Type u_1<VAR>Field K<VAR>L : Type u_2<VAR>CommRing L<VAR>IsDomain L<VAR>Algebra K L<VAR>IsCyclotomicExtension {n} K L<VAR>h : Irreducible (Polynomial.cyclotomic (↑n) K)<VAR>t : (ZMod ↑n)ˣ<GOAL>(IsCyclotomicExtension.autEquivPow L h).symm t = (IsPrimitiveRoot.powerBasis K ⋯).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) ⋯
<VAR>n : ℕ+<VAR>K : Type u_1<VAR>Field K<VAR>L : Type u_2<VAR>μ : L<VAR>CommRing L<VAR>IsDomain L<VAR>hμ : IsPrimitiveRoot μ ↑n<VAR>Algebra K L<VAR>IsCyclotomicExtension {n} K L<VAR>h : Irreducible (Polynomial.cyclotomic (↑n) K)<GOAL>(IsCyclotomicExtension.fromZetaAut hμ h) (IsCyclotomicExtension.zeta n K L) = μ
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<GOAL>PadicInt.modPart p r < ↑p
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<GOAL>0 ≤ PadicInt.modPart p r
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>h : ‖↑r‖ ≤ 1<GOAL>IsUnit ↑r.den
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>h : ‖↑r‖ ≤ 1<GOAL>↑p ∣ r.num - r.num * r.den.gcdA p % ↑p * ↑r.den
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>h : ‖↑r‖ ≤ 1<GOAL>‖⟨↑r, h⟩ - ↑(PadicInt.modPart p r)‖ < 1
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>h : ‖↑r‖ ≤ 1<GOAL>∃ n, 0 ≤ n ∧ n < ↑p ∧ ‖⟨↑r, h⟩ - ↑n‖ < 1