ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>z : ℤ<GOAL>‖↑z‖ = ‖↑z‖
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>q : ℚ_[p]<VAR>hq : ‖q‖ ≤ 1<GOAL>‖⟨q, hq⟩‖ = ‖q‖
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<GOAL>‖↑p‖ = (↑p)⁻¹
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>‖↑p ^ n‖ = ↑p ^ (-↑n)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : ℤ<GOAL>‖↑k‖ < 1 ↔ ↑p ∣ k
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : ℤ<VAR>n : ℕ<GOAL>‖↑k‖ ≤ ↑p ^ (-↑n) ↔ ↑p ^ n ∣ k
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>PadicInt.valuation 0 = 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>PadicInt.valuation 1 = 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ℤ_[p]<GOAL>0 ≤ x.valuation
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>z : ℤ_[p]<GOAL>‖z‖ = 1 → z * z.inv = 1
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>z : ℤ_[p]<GOAL>IsUnit z ↔ ‖z‖ = 1
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>z1 z2 : ℤ_[p]<VAR>hz1 : ‖z1‖ < 1<VAR>hz2 : ‖z2‖ < 1<GOAL>‖z1 + z2‖ < 1
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>z1 z2 : ℤ_[p]<VAR>hz2 : ‖z2‖ < 1<GOAL>‖z1 * z2‖ < 1
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>u : ℚ_[p]<VAR>h : ‖u‖ = 1<GOAL>↑↑(PadicInt.mkUnits h) = u
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>u : ℤ_[p]ˣ<GOAL>‖↑u‖ = 1
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ℤ_[p]<VAR>hx : x ≠ 0<GOAL>↑↑(PadicInt.unitCoeff hx) = ↑x * ↑p ^ (-x.valuation)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ℤ_[p]<VAR>hx : x ≠ 0<GOAL>x = ↑(PadicInt.unitCoeff hx) * ↑p ^ x.valuation.natAbs
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ℤ_[p]<VAR>n : ℕ<GOAL>‖x‖ ≤ ↑p ^ (-↑n) ↔ x ∈ Ideal.span {↑p ^ n}
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>LocalRing.maximalIdeal ℤ_[p] = Ideal.span {↑p}
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>Irreducible ↑p
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>s : Ideal ℤ_[p]<VAR>hs : s ≠ ⊥<GOAL>∃ n, s = Ideal.span {↑p ^ n}
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ℤ_[p]<GOAL>(algebraMap ℤ_[p] ℚ_[p]) x = ↑x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>self : WeakFEPair E<GOAL>MeasureTheory.LocallyIntegrableOn self.g (Set.Ioi 0) MeasureTheory.volume
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>self : WeakFEPair E<VAR>x : ℝ<GOAL>x ∈ Set.Ioi 0 → self.f (1 / x) = (self.ε * ↑(x ^ self.k)) • self.g x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>self : WeakFEPair E<VAR>r : ℝ<GOAL>(fun x => self.f x - self.f₀) =O[Filter.atTop] fun x => x ^ r
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>self : WeakFEPair E<VAR>r : ℝ<GOAL>(fun x => self.g x - self.g₀) =O[Filter.atTop] fun x => x ^ r
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>self : WeakFEPair E<GOAL>self.ε ≠ 0
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>self : WeakFEPair E<GOAL>0 < self.k
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>self : WeakFEPair E<GOAL>MeasureTheory.LocallyIntegrableOn self.f (Set.Ioi 0) MeasureTheory.volume
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>self : StrongFEPair E<GOAL>self.g₀ = 0
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>self : StrongFEPair E<GOAL>self.f₀ = 0
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>P : WeakFEPair E<VAR>x : ℝ<VAR>hx : 0 < x<GOAL>P.g (1 / x) = (P.ε⁻¹ * ↑(x ^ P.k)) • P.f x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>P : WeakFEPair E<VAR>r : ℝ<GOAL>(fun x => P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀) =O[𝓝[>] 0] fun x => x ^ r
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>P : WeakFEPair E<GOAL>(fun x => P.f x - P.f₀) =O[𝓝[>] 0] fun x => x ^ (-P.k)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>P : StrongFEPair E<VAR>r : ℝ<GOAL>P.f =O[Filter.atTop] fun x => x ^ r
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>P : StrongFEPair E<VAR>r : ℝ<GOAL>P.f =O[𝓝[>] 0] fun x => x ^ r
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>P : StrongFEPair E<VAR>s : ℂ<GOAL>HasMellin P.f s (P.Λ s)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>P : StrongFEPair E<GOAL>P.Λ = mellin P.f
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>P : StrongFEPair E<GOAL>P.symm.Λ = mellin P.g
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>P : StrongFEPair E<GOAL>Differentiable ℂ P.Λ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>P : StrongFEPair E<VAR>s : ℂ<GOAL>P.Λ (↑P.k - s) = P.ε • P.symm.Λ s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>P : WeakFEPair E<GOAL>MeasureTheory.LocallyIntegrableOn P.f_modif (Set.Ioi 0) MeasureTheory.volume
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>P : WeakFEPair E<VAR>x : ℝ<VAR>hx : 0 < x<GOAL>P.f_modif (1 / x) = (P.ε * ↑(x ^ P.k)) • P.g_modif x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>P : WeakFEPair E<GOAL>Set.EqOn (fun x => P.f_modif x - P.f x + P.f₀) (((Set.Ioo 0 1).indicator fun x => P.f₀ - (P.ε * ↑(x ^ (-P.k))) • P.g₀) + {1}.indicator fun x => P.f₀ - P.f 1) (Set.Ioi 0)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>P : WeakFEPair E<VAR>s : ℂ<VAR>hs : P.k < s.re<GOAL>mellin (fun x => P.f_modif x - P.f x + P.f₀) s = (1 / s) • P.f₀ + (P.ε / (↑P.k - s)) • P.g₀
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>P : WeakFEPair E<VAR>s : ℂ<GOAL>P.Λ₀ s = P.Λ s + (1 / s) • P.f₀ + (P.ε / (↑P.k - s)) • P.g₀
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>P : WeakFEPair E<VAR>s : ℂ<GOAL>P.symm.Λ₀ s = P.symm.Λ s + (1 / s) • P.g₀ + (P.ε⁻¹ / (↑P.k - s)) • P.f₀
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>P : WeakFEPair E<GOAL>Differentiable ℂ P.Λ₀
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>P : WeakFEPair E<VAR>s : ℂ<VAR>hs : s ≠ 0 ∨ P.f₀ = 0<VAR>hs' : s ≠ ↑P.k ∨ P.g₀ = 0<GOAL>DifferentiableAt ℂ P.Λ s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>P : WeakFEPair E<VAR>s : ℂ<VAR>hs : P.k < s.re<GOAL>HasMellin (fun x => P.f x - P.f₀) s (P.Λ s)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>P : WeakFEPair E<VAR>s : ℂ<GOAL>P.Λ₀ (↑P.k - s) = P.ε • P.symm.Λ₀ s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>P : WeakFEPair E<VAR>s : ℂ<GOAL>P.Λ (↑P.k - s) = P.ε • P.symm.Λ s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>P : WeakFEPair E<GOAL>Filter.Tendsto (fun s => (s - ↑P.k) • P.Λ s) (𝓝[≠] ↑P.k) (𝓝 (P.ε • P.g₀))
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>P : WeakFEPair E<GOAL>Filter.Tendsto (fun s => s • P.Λ s) (𝓝[≠] 0) (𝓝 (-P.f₀))
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hpi : Prime ↑p<GOAL>p % 4 = 3
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hp3 : p % 4 = 3<GOAL>Prime ↑p
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<GOAL>Prime ↑p ↔ p % 4 = 3
<VAR>n : ℕ<GOAL>deriv Real.Gamma (↑n + 1) = ↑n ! * (-γ + ↑(harmonic n))
<VAR>n : ℕ<GOAL>HasDerivAt Real.Gamma (↑n ! * (-γ + ↑(harmonic n))) (↑n + 1)
<GOAL>HasDerivAt Real.Gamma (-√Real.pi * (γ + 2 * Real.log 2)) (1 / 2)
<VAR>n : ℕ<GOAL>DifferentiableAt ℂ Complex.Gamma (↑n + 1)
<VAR>n : ℕ<GOAL>HasDerivAt Complex.Gamma (↑n ! * (-↑γ + ↑(harmonic n))) (↑n + 1)
<VAR>n : ℕ<GOAL>deriv Complex.Gamma (↑n + 1) = ↑n ! * (-↑γ + ↑(harmonic n))
<GOAL>HasDerivAt Complex.Gamma (-↑√Real.pi * (↑γ + 2 * Complex.log 2)) (1 / 2)
<GOAL>HasDerivAt Complex.Gammaℂ (-(↑γ + Complex.log (2 * ↑Real.pi)) / ↑Real.pi) 1
<GOAL>HasDerivAt Complex.Gammaℝ (-(↑γ + Complex.log (4 * ↑Real.pi)) / 2) 1
<VAR>K : Type u<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<GOAL>IsPrincipalIdealRing (NumberField.RingOfIntegers K)
<VAR>K : Type u<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {5} ℚ K<GOAL>IsPrincipalIdealRing (NumberField.RingOfIntegers K)
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<GOAL>Function.Injective ⇑(NumberField.canonicalEmbedding K)
<VAR>K : Type u_1<VAR>Field K<VAR>φ : K →+* ℂ<VAR>x : K<GOAL>(NumberField.canonicalEmbedding K) x φ = φ x
<VAR>K : Type u_1<VAR>Field K<VAR>x : (K →+* ℂ) → ℂ<VAR>φ : K →+* ℂ<VAR>hx : x ∈ Submodule.span ℝ (Set.range ⇑(NumberField.canonicalEmbedding K))<GOAL>(starRingEnd ℂ) (x φ) = x (NumberField.ComplexEmbedding.conjugate φ)
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>x : K<GOAL>‖(NumberField.canonicalEmbedding K) x‖₊ = Finset.univ.sup fun φ => ‖φ x‖₊
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>x : K<VAR>r : ℝ<GOAL>‖(NumberField.canonicalEmbedding K) x‖ ≤ r ↔ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>r : ℝ<GOAL>(↑(NumberField.canonicalEmbedding.integerLattice K) ∩ Metric.closedBall 0 r).Finite
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>i : Module.Free.ChooseBasisIndex ℤ (NumberField.RingOfIntegers K)<GOAL>(NumberField.canonicalEmbedding.latticeBasis K) i = (NumberField.canonicalEmbedding K) ((NumberField.integralBasis K) i)
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>x : (K →+* ℂ) → ℂ<GOAL>x ∈ Submodule.span ℤ (Set.range ⇑(NumberField.canonicalEmbedding.latticeBasis K)) ↔ x ∈ ((NumberField.canonicalEmbedding K).comp (algebraMap (NumberField.RingOfIntegers K) K)).range
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>x : K<GOAL>(NumberField.canonicalEmbedding K) x ∈ Submodule.span ℚ (Set.range ⇑(NumberField.canonicalEmbedding.latticeBasis K))
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>x : K<VAR>i : Module.Free.ChooseBasisIndex ℤ (NumberField.RingOfIntegers K)<GOAL>((NumberField.canonicalEmbedding.latticeBasis K).repr ((NumberField.canonicalEmbedding K) x)) i = ↑(((NumberField.integralBasis K).repr x) i)
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<GOAL>FiniteDimensional.finrank ℝ (({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)) = FiniteDimensional.finrank ℚ K
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<GOAL>Function.Injective ⇑(NumberField.mixedEmbedding K)
<VAR>K : Type u_1<VAR>Field K<VAR>x : (K →+* ℂ) → ℂ<VAR>w : NumberField.InfinitePlace K<VAR>hw : w.IsReal<GOAL>((NumberField.mixedEmbedding.commMap K) x).1 ⟨w, hw⟩ = (x w.embedding).re
<VAR>K : Type u_1<VAR>Field K<VAR>x : (K →+* ℂ) → ℂ<VAR>w : NumberField.InfinitePlace K<VAR>hw : w.IsComplex<GOAL>((NumberField.mixedEmbedding.commMap K) x).2 ⟨w, hw⟩ = x w.embedding
<VAR>K : Type u_1<VAR>Field K<VAR>x : K<GOAL>(NumberField.mixedEmbedding.commMap K) ((NumberField.canonicalEmbedding K) x) = (NumberField.mixedEmbedding K) x
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<GOAL>Disjoint (Submodule.span ℝ (Set.range ⇑(NumberField.canonicalEmbedding.latticeBasis K))) (LinearMap.ker (NumberField.mixedEmbedding.commMap K))
<VAR>K : Type u_1<VAR>Field K<VAR>w : NumberField.InfinitePlace K<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>0 ≤ (NumberField.mixedEmbedding.normAtPlace w) x
<VAR>K : Type u_1<VAR>Field K<VAR>w : NumberField.InfinitePlace K<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>(NumberField.mixedEmbedding.normAtPlace w) (-x) = (NumberField.mixedEmbedding.normAtPlace w) x
<VAR>K : Type u_1<VAR>Field K<VAR>w : NumberField.InfinitePlace K<VAR>x y : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>(NumberField.mixedEmbedding.normAtPlace w) (x + y) ≤ (NumberField.mixedEmbedding.normAtPlace w) x + (NumberField.mixedEmbedding.normAtPlace w) y
<VAR>K : Type u_1<VAR>Field K<VAR>w : NumberField.InfinitePlace K<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<VAR>c : ℝ<GOAL>(NumberField.mixedEmbedding.normAtPlace w) (c • x) = |c| * (NumberField.mixedEmbedding.normAtPlace w) x
<VAR>K : Type u_1<VAR>Field K<VAR>w : NumberField.InfinitePlace K<VAR>c : ℝ<GOAL>(NumberField.mixedEmbedding.normAtPlace w) (fun x => c, fun x => ↑c) = |c|
<VAR>K : Type u_1<VAR>Field K<VAR>w : NumberField.InfinitePlace K<VAR>hw : w.IsReal<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>(NumberField.mixedEmbedding.normAtPlace w) x = ‖x.1 ⟨w, hw⟩‖
<VAR>K : Type u_1<VAR>Field K<VAR>w : NumberField.InfinitePlace K<VAR>hw : w.IsComplex<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>(NumberField.mixedEmbedding.normAtPlace w) x = ‖x.2 ⟨w, hw⟩‖
<VAR>K : Type u_1<VAR>Field K<VAR>w : NumberField.InfinitePlace K<VAR>x : K<GOAL>(NumberField.mixedEmbedding.normAtPlace w) ((NumberField.mixedEmbedding K) x) = w x
<VAR>K : Type u_1<VAR>Field K<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>(∀ (w : NumberField.InfinitePlace K), (NumberField.mixedEmbedding.normAtPlace w) x = 0) ↔ x = 0
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>‖x‖₊ = Finset.univ.sup fun w => ⟨(NumberField.mixedEmbedding.normAtPlace w) x, ⋯⟩
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>‖x‖ = Finset.univ.sup' ⋯ fun w => (NumberField.mixedEmbedding.normAtPlace w) x
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>NumberField.mixedEmbedding.norm x = ∏ w : NumberField.InfinitePlace K, (NumberField.mixedEmbedding.normAtPlace w) x ^ w.mult
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>0 ≤ NumberField.mixedEmbedding.norm x
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>NumberField.mixedEmbedding.norm x = 0 ↔ ∃ w, (NumberField.mixedEmbedding.normAtPlace w) x = 0
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>NumberField.mixedEmbedding.norm x ≠ 0 ↔ ∀ (w : NumberField.InfinitePlace K), (NumberField.mixedEmbedding.normAtPlace w) x ≠ 0
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>c : ℝ<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>NumberField.mixedEmbedding.norm (c • x) = |c| ^ FiniteDimensional.finrank ℚ K * NumberField.mixedEmbedding.norm x
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>c : ℝ<GOAL>NumberField.mixedEmbedding.norm (fun x => c, fun x => ↑c) = |c| ^ FiniteDimensional.finrank ℚ K
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>x : K<GOAL>NumberField.mixedEmbedding.norm ((NumberField.mixedEmbedding K) x) = ↑|(Algebra.norm ℚ) x|
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<VAR>hx : x ∈ Set.range ⇑(NumberField.mixedEmbedding K)<GOAL>NumberField.mixedEmbedding.norm x = 0 ↔ x = 0
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<VAR>w : { w // w.IsReal }<GOAL>((NumberField.mixedEmbedding.stdBasis K).repr x) (Sum.inl w) = x.1 w
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<VAR>w : { w // w.IsComplex }<GOAL>((NumberField.mixedEmbedding.stdBasis K).repr x) (Sum.inr (w, 0)) = (x.2 w).re
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<VAR>w : { w // w.IsComplex }<GOAL>((NumberField.mixedEmbedding.stdBasis K).repr x) (Sum.inr (w, 1)) = (x.2 w).im
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<GOAL>Zspan.fundamentalDomain (NumberField.mixedEmbedding.stdBasis K) = (Set.univ.pi fun x => Set.Ico 0 1) ×ˢ Set.univ.pi fun x => ⇑Complex.measurableEquivPi ⁻¹' Set.univ.pi fun x => Set.Ico 0 1
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<GOAL>MeasureTheory.volume (Zspan.fundamentalDomain (NumberField.mixedEmbedding.stdBasis K)) = 1
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>w : { w // w.IsReal }<GOAL>(NumberField.mixedEmbedding.indexEquiv K) (Sum.inl w) = (↑w).embedding
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>w : { w // w.IsComplex }<GOAL>(NumberField.mixedEmbedding.indexEquiv K) (Sum.inr (w, 0)) = (↑w).embedding
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>w : { w // w.IsComplex }<GOAL>(NumberField.mixedEmbedding.indexEquiv K) (Sum.inr (w, 1)) = NumberField.ComplexEmbedding.conjugate (↑w).embedding
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<GOAL>(NumberField.mixedEmbedding.matrixToStdBasis K).det = (2⁻¹ * Complex.I) ^ NumberField.InfinitePlace.NrComplexPlaces K
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>x : (K →+* ℂ) → ℂ<VAR>hx : ∀ (φ : K →+* ℂ), (starRingEnd ℂ) (x φ) = x (NumberField.ComplexEmbedding.conjugate φ)<VAR>c : NumberField.mixedEmbedding.index K<GOAL>↑(((NumberField.mixedEmbedding.stdBasis K).repr ((NumberField.mixedEmbedding.commMap K) x)) c) = (NumberField.mixedEmbedding.matrixToStdBasis K).mulVec (x ∘ ⇑(NumberField.mixedEmbedding.indexEquiv K)) c
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>i : Module.Free.ChooseBasisIndex ℤ (NumberField.RingOfIntegers K)<GOAL>(NumberField.mixedEmbedding.latticeBasis K) i = (NumberField.mixedEmbedding K) ((NumberField.integralBasis K) i)
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>x ∈ Submodule.span ℤ (Set.range ⇑(NumberField.mixedEmbedding.latticeBasis K)) ↔ x ∈ ((NumberField.mixedEmbedding K).comp (algebraMap (NumberField.RingOfIntegers K) K)).range
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>x : K<GOAL>(NumberField.mixedEmbedding K) x ∈ Submodule.span ℚ (Set.range ⇑(NumberField.mixedEmbedding.latticeBasis K))
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>x : K<VAR>i : Module.Free.ChooseBasisIndex ℤ (NumberField.RingOfIntegers K)<GOAL>((NumberField.mixedEmbedding.latticeBasis K).repr ((NumberField.mixedEmbedding K) x)) i = ↑(((NumberField.integralBasis K).repr x) i)
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ<VAR>e : Module.Free.ChooseBasisIndex ℤ (NumberField.RingOfIntegers K) ≃ Module.Free.ChooseBasisIndex ℤ ↥↑↑I<GOAL>|(NumberField.mixedEmbedding.latticeBasis K).det (⇑(NumberField.mixedEmbedding K) ∘ ⇑(NumberField.basisOfFractionalIdeal K I) ∘ ⇑e)| = ↑(FractionalIdeal.absNorm ↑I)
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ<VAR>i : Module.Free.ChooseBasisIndex ℤ ↥↑↑I<GOAL>(NumberField.mixedEmbedding.fractionalIdealLatticeBasis K I) i = (NumberField.mixedEmbedding K) ((NumberField.basisOfFractionalIdeal K I) i)
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>x ∈ Submodule.span ℤ (Set.range ⇑(NumberField.mixedEmbedding.fractionalIdealLatticeBasis K I)) ↔ x ∈ ⇑(NumberField.mixedEmbedding K) '' ↑↑I
<VAR>x : ℤ[i]<GOAL>GaussianInt.toComplex x = ↑x.re + ↑x.im * Complex.I
<VAR>x y : ℤ<GOAL>GaussianInt.toComplex { re := x, im := y } = ↑x + ↑y * Complex.I
<VAR>x : ℤ[i]<GOAL>GaussianInt.toComplex x = { re := ↑x.re, im := ↑x.im }
<VAR>x : ℤ[i]<GOAL>↑x.re = (GaussianInt.toComplex x).re
<VAR>x : ℤ[i]<GOAL>↑x.im = (GaussianInt.toComplex x).im
<VAR>x y : ℤ<GOAL>(GaussianInt.toComplex { re := x, im := y }).re = ↑x
<VAR>x y : ℤ<GOAL>(GaussianInt.toComplex { re := x, im := y }).im = ↑y
<VAR>x y : ℤ[i]<GOAL>GaussianInt.toComplex (x + y) = GaussianInt.toComplex x + GaussianInt.toComplex y
<VAR>x y : ℤ[i]<GOAL>GaussianInt.toComplex (x * y) = GaussianInt.toComplex x * GaussianInt.toComplex y
<VAR>x : ℤ[i]<GOAL>GaussianInt.toComplex (-x) = -GaussianInt.toComplex x
<VAR>x y : ℤ[i]<GOAL>GaussianInt.toComplex (x - y) = GaussianInt.toComplex x - GaussianInt.toComplex y
<VAR>x : ℤ[i]<GOAL>GaussianInt.toComplex (star x) = (starRingEnd ℂ) (GaussianInt.toComplex x)
<VAR>x y : ℤ[i]<GOAL>GaussianInt.toComplex x = GaussianInt.toComplex y ↔ x = y
<GOAL>Function.Injective ⇑GaussianInt.toComplex
<VAR>x : ℤ[i]<GOAL>GaussianInt.toComplex x = 0 ↔ x = 0
<VAR>x : ℤ[i]<GOAL>↑(Zsqrtd.norm x) = Complex.normSq (GaussianInt.toComplex x)
<VAR>x : ℤ[i]<GOAL>↑(Zsqrtd.norm x) = ↑(Complex.normSq (GaussianInt.toComplex x))
<VAR>x : ℤ[i]<GOAL>0 ≤ Zsqrtd.norm x
<VAR>x : ℤ[i]<GOAL>Zsqrtd.norm x = 0 ↔ x = 0
<VAR>x : ℤ[i]<GOAL>0 < Zsqrtd.norm x ↔ x ≠ 0
<VAR>x : ℤ[i]<GOAL>↑(Zsqrtd.norm x).natAbs = Zsqrtd.norm x
<VAR>α : Type u_1<VAR>Ring α<VAR>x : ℤ[i]<GOAL>↑(Zsqrtd.norm x).natAbs = ↑(Zsqrtd.norm x)
<VAR>x : ℤ[i]<GOAL>(Zsqrtd.norm x).natAbs = x.re.natAbs * x.re.natAbs + x.im.natAbs * x.im.natAbs
<VAR>x y : ℤ[i]<GOAL>x / y = { re := round (↑(x * star y).re / ↑(Zsqrtd.norm y)), im := round (↑(x * star y).im / ↑(Zsqrtd.norm y)) }
<VAR>x y : ℤ[i]<GOAL>(GaussianInt.toComplex (x / y)).re = ↑(round (GaussianInt.toComplex x / GaussianInt.toComplex y).re)
<VAR>x y : ℤ[i]<GOAL>(GaussianInt.toComplex (x / y)).im = ↑(round (GaussianInt.toComplex x / GaussianInt.toComplex y).im)
<VAR>x y : ℂ<VAR>hre : |x.re| ≤ |y.re|<VAR>him : |x.im| ≤ |y.im|<GOAL>Complex.normSq x ≤ Complex.normSq y
<VAR>x y : ℤ[i]<GOAL>Complex.normSq (GaussianInt.toComplex x / GaussianInt.toComplex y - GaussianInt.toComplex (x / y)) < 1
<VAR>x y : ℤ[i]<GOAL>x % y = x - y * (x / y)
<VAR>x : ℤ[i]<VAR>y : ℤ[i]<VAR>hy : y ≠ 0<GOAL>Zsqrtd.norm (x % y) < Zsqrtd.norm y
<VAR>x : ℤ[i]<VAR>y : ℤ[i]<VAR>hy : y ≠ 0<GOAL>(Zsqrtd.norm (x % y)).natAbs < (Zsqrtd.norm y).natAbs
<VAR>x : ℤ[i]<VAR>y : ℤ[i]<VAR>hy : y ≠ 0<GOAL>(Zsqrtd.norm x).natAbs ≤ (Zsqrtd.norm (x * y)).natAbs
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hpi : ¬Irreducible ↑p<GOAL>∃ a b, a ^ 2 + b ^ 2 = p
<VAR>L : Type u<VAR>CommRing L<VAR>IsDomain L<VAR>n : ℕ+<VAR>g : L ≃+* L<GOAL>∃ m, ∀ (t : ↥(rootsOfUnity n L)), g ↑↑t = ↑(↑t ^ m)
<VAR>L : Type u<VAR>CommRing L<VAR>IsDomain L<VAR>n : ℕ+<VAR>g : L ≃+* L<GOAL>∃ m, ∀ t ∈ rootsOfUnity n L, g ↑t = ↑(t ^ m)
<VAR>L : Type u<VAR>CommRing L<VAR>IsDomain L<VAR>g : L ≃+* L<VAR>n : ℕ+<VAR>t : ↥(rootsOfUnity n L)<GOAL>g ↑↑t = ↑(↑t ^ ModularCyclotomicCharacter_aux g n)
<VAR>L : Type u<VAR>CommRing L<VAR>IsDomain L<VAR>g : L ≃+* L<VAR>n : ℕ+<VAR>t : ↥(rootsOfUnity n L)<GOAL>g ↑↑t = ↑(↑t ^ (ModularCyclotomicCharacter.toFun n g).val)
<VAR>L : Type u<VAR>CommRing L<VAR>IsDomain L<VAR>g : L ≃+* L<VAR>n : ℕ+<VAR>t : Lˣ<VAR>ht : t ∈ rootsOfUnity n L<GOAL>g ↑t = ↑t ^ (ModularCyclotomicCharacter.toFun n g).val
<VAR>L : Type u<VAR>CommRing L<VAR>IsDomain L<VAR>g : L ≃+* L<VAR>n : ℕ+<VAR>t : L<VAR>ht : IsPrimitiveRoot t ↑n<GOAL>g t = t ^ (ModularCyclotomicCharacter.toFun n g).val
<VAR>L : Type u<VAR>CommRing L<VAR>IsDomain L<VAR>n : ℕ+<VAR>g : L ≃+* L<VAR>c : ZMod (Fintype.card ↥(rootsOfUnity n L))<VAR>hc : ∀ (t : ↥(rootsOfUnity n L)), g ↑↑t = ↑(↑t ^ c.val)<GOAL>c = ModularCyclotomicCharacter.toFun n g
<VAR>L : Type u<VAR>CommRing L<VAR>IsDomain L<VAR>n : ℕ+<VAR>g : L ≃+* L<VAR>c : ZMod (Fintype.card ↥(rootsOfUnity n L))<VAR>hc : ∀ t ∈ rootsOfUnity n L, g ↑t = ↑t ^ c.val<GOAL>c = ModularCyclotomicCharacter.toFun n g
<VAR>L : Type u<VAR>CommRing L<VAR>IsDomain L<VAR>n : ℕ+<GOAL>ModularCyclotomicCharacter.toFun n (RingEquiv.refl L) = 1
<VAR>L : Type u<VAR>CommRing L<VAR>IsDomain L<VAR>n : ℕ+<VAR>g h : L ≃+* L<GOAL>ModularCyclotomicCharacter.toFun n (g * h) = ModularCyclotomicCharacter.toFun n g * ModularCyclotomicCharacter.toFun n h
<VAR>L : Type u<VAR>CommRing L<VAR>IsDomain L<VAR>n : ℕ+<VAR>g : L ≃+* L<VAR>t : Lˣ<VAR>ht : t ∈ rootsOfUnity n L<GOAL>g ↑t = ↑t ^ (↑((ModularCyclotomicCharacter' L n) g)).val
<VAR>L : Type u<VAR>CommRing L<VAR>IsDomain L<VAR>n : ℕ+<VAR>g : L ≃+* L<VAR>c : ZMod (Fintype.card ↥(rootsOfUnity n L))<VAR>hc : ∀ t ∈ rootsOfUnity n L, g ↑t = ↑t ^ c.val<GOAL>c = ↑((ModularCyclotomicCharacter' L n) g)
<VAR>L : Type u<VAR>CommRing L<VAR>IsDomain L<VAR>n : ℕ+<VAR>hn : Fintype.card ↥(rootsOfUnity n L) = ↑n<VAR>g : L ≃+* L<VAR>t : Lˣ<VAR>ht : t ∈ rootsOfUnity n L<GOAL>g ↑t = ↑t ^ (↑((ModularCyclotomicCharacter L hn) g)).val
<VAR>L : Type u<VAR>CommRing L<VAR>IsDomain L<VAR>n : ℕ+<VAR>hn : Fintype.card ↥(rootsOfUnity n L) = ↑n<VAR>g : L ≃+* L<VAR>c : ZMod ↑n<VAR>hc : ∀ t ∈ rootsOfUnity n L, g ↑t = ↑t ^ c.val<GOAL>c = ↑((ModularCyclotomicCharacter L hn) g)
<VAR>L : Type u<VAR>CommRing L<VAR>IsDomain L<VAR>n : ℕ+<VAR>R : Type u_1<VAR>CommRing R<VAR>Algebra R L<VAR>μ : L<VAR>hμ : IsPrimitiveRoot μ ↑n<VAR>g : L ≃ₐ[R] L<GOAL>(IsPrimitiveRoot.autToPow R hμ) g = (ModularCyclotomicCharacter L ⋯) ↑g
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>A : Type u_2<VAR>Field A<VAR>CharZero A<VAR>IsAlgClosed A<GOAL>Fintype.card (K →+* A) = FiniteDimensional.finrank ℚ K