ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>Q : Type u_4<VAR>L.Structure M<VAR>L.Structure N<VAR>L.Structure P<VAR>L.Structure Q<VAR>f : M ↪ₑ[L] N<VAR>g : N ↪ₑ[L] P<VAR>h : P ↪ₑ[L] Q<GOAL>(h.comp g).comp f = h.comp (g.comp f)
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>L.Structure M<VAR>N : Type u_5<VAR>L.Structure N<VAR>L[[M]].Structure N<VAR>(L.lhomWithConstants M).IsExpansionOn N<VAR>N ⊨ L.elementaryDiagram M<GOAL>∀ (a : M), (FirstOrder.Language.ElementaryEmbedding.ofModelsElementaryDiagram L M N) a = (FirstOrder.Language.constantMap ∘ Sum.inr) a
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>N : Type u_2<VAR>L.Structure M<VAR>L.Structure N<VAR>f : M ↪[L] N<VAR>htv : ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N), φ.Realize default (Fin.snoc (⇑f ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (⇑f ∘ x) (f b))<VAR>n : ℕ<VAR>φ : L.Formula (Fin n)<VAR>x : Fin n → M<GOAL>φ.Realize (⇑f ∘ x) ↔ φ.Realize x
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>N : Type u_2<VAR>L.Structure M<VAR>L.Structure N<VAR>f : M ↪[L] N<VAR>htv : ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N), φ.Realize default (Fin.snoc (⇑f ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (⇑f ∘ x) (f b))<VAR>a : M<GOAL>(f.toElementaryEmbedding htv) a = f a
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>N : Type u_2<VAR>L.Structure M<VAR>L.Structure N<VAR>f : M ≃[L] N<GOAL>f.toElementaryEmbedding.toEmbedding = f.toEmbedding
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>N : Type u_2<VAR>L.Structure M<VAR>L.Structure N<VAR>f : M ≃[L] N<GOAL>⇑f.toElementaryEmbedding = ⇑f
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>L.Structure M<VAR>α : Type u_5<VAR>S : L.Substructure M<VAR>v : α → ↥S<VAR>t : L.Term α<GOAL>FirstOrder.Language.Term.realize (Subtype.val ∘ v) t = ↑(FirstOrder.Language.Term.realize v t)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℝ → E<VAR>a b : ℝ<GOAL>⨍ (x : ℝ) in a..b, f x = ⨍ (x : ℝ) in b..a, f x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℝ → E<VAR>a b : ℝ<GOAL>⨍ (x : ℝ) in a..b, f x = (b - a)⁻¹ • ∫ (x : ℝ) in a..b, f x
<VAR>f : ℝ → ℝ<VAR>a b : ℝ<GOAL>⨍ (x : ℝ) in a..b, f x = (∫ (x : ℝ) in a..b, f x) / (b - a)
<VAR>a : ℝ<VAR>b : ℝ<VAR>h : 0 < b<GOAL>MeasureTheory.IntegrableOn (fun x => rexp (-b * x)) (Set.Ioi a) MeasureTheory.volume
<VAR>f : ℝ → ℝ<VAR>a b : ℝ<VAR>h0 : 0 < b<VAR>hf : ContinuousOn f (Set.Ici a)<VAR>ho : f =O[Filter.atTop] fun x => rexp (-b * x)<GOAL>MeasureTheory.IntegrableOn f (Set.Ioi a) MeasureTheory.volume
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>n : ℕ<VAR>φ : L.BoundedFormula α (n + 1)<GOAL>¬φ.all.IsAtomic
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>n : ℕ<VAR>φ : L.BoundedFormula α (n + 1)<GOAL>¬φ.ex.IsAtomic
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>β : Type v'<VAR>n m : ℕ<VAR>φ : L.BoundedFormula α m<VAR>h : φ.IsAtomic<VAR>f : α → β ⊕ Fin n<GOAL>(FirstOrder.Language.BoundedFormula.relabel f φ).IsAtomic
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>l : ℕ<VAR>φ : L.BoundedFormula α l<VAR>k m : ℕ<VAR>h : φ.IsAtomic<GOAL>(FirstOrder.Language.BoundedFormula.liftAt k m φ).IsAtomic
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>n l : ℕ<VAR>φ : L.BoundedFormula α l<VAR>h : l ≤ n<VAR>hφ : φ.IsAtomic<GOAL>(FirstOrder.Language.BoundedFormula.castLE h φ).IsAtomic
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>n : ℕ<VAR>φ : L.BoundedFormula α n<GOAL>φ.IsAtomic → φ.IsQF
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>n : ℕ<GOAL>⊥.IsQF
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>n : ℕ<VAR>φ : L.BoundedFormula α n<VAR>h : φ.IsQF<GOAL>φ.not.IsQF
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>β : Type v'<VAR>n m : ℕ<VAR>φ : L.BoundedFormula α m<VAR>h : φ.IsQF<VAR>f : α → β ⊕ Fin n<GOAL>(FirstOrder.Language.BoundedFormula.relabel f φ).IsQF
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>l : ℕ<VAR>φ : L.BoundedFormula α l<VAR>k m : ℕ<VAR>h : φ.IsQF<GOAL>(FirstOrder.Language.BoundedFormula.liftAt k m φ).IsQF
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>n l : ℕ<VAR>φ : L.BoundedFormula α l<VAR>h : l ≤ n<VAR>hφ : φ.IsQF<GOAL>(FirstOrder.Language.BoundedFormula.castLE h φ).IsQF
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>n : ℕ<VAR>φ : L.BoundedFormula α (n + 1)<GOAL>¬φ.all.IsQF
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>n : ℕ<VAR>φ : L.BoundedFormula α (n + 1)<GOAL>¬φ.ex.IsQF
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>n : ℕ<VAR>φ : L.BoundedFormula α n<GOAL>φ.IsQF → φ.IsPrenex
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>n : ℕ<VAR>φ : L.BoundedFormula α n<VAR>h : φ.IsAtomic<GOAL>φ.IsPrenex
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>n : ℕ<VAR>P : {n : ℕ} → L.BoundedFormula α n → Prop<VAR>φ : L.BoundedFormula α n<VAR>h : φ.IsPrenex<VAR>hq : ∀ {m : ℕ} {ψ : L.BoundedFormula α m}, ψ.IsQF → P ψ<VAR>ha : ∀ {m : ℕ} {ψ : L.BoundedFormula α (m + 1)}, P ψ → P ψ.all<VAR>hn : ∀ {m : ℕ} {ψ : L.BoundedFormula α m}, P ψ → P ψ.not<GOAL>P φ
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>β : Type v'<VAR>n m : ℕ<VAR>φ : L.BoundedFormula α m<VAR>h : φ.IsPrenex<VAR>f : α → β ⊕ Fin n<GOAL>(FirstOrder.Language.BoundedFormula.relabel f φ).IsPrenex
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>l : ℕ<VAR>φ : L.BoundedFormula α l<VAR>hφ : φ.IsPrenex<VAR>n : ℕ<VAR>h : l ≤ n<GOAL>(FirstOrder.Language.BoundedFormula.castLE h φ).IsPrenex
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>l : ℕ<VAR>φ : L.BoundedFormula α l<VAR>k m : ℕ<VAR>h : φ.IsPrenex<GOAL>(FirstOrder.Language.BoundedFormula.liftAt k m φ).IsPrenex
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>n : ℕ<VAR>φ ψ : L.BoundedFormula α n<GOAL>ψ.IsQF → φ.toPrenexImpRight ψ = φ.imp ψ
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>n : ℕ<VAR>φ ψ : L.BoundedFormula α n<VAR>hφ : φ.IsQF<VAR>hψ : ψ.IsPrenex<GOAL>(φ.toPrenexImpRight ψ).IsPrenex
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>n : ℕ<VAR>φ ψ : L.BoundedFormula α n<GOAL>φ.IsQF → φ.toPrenexImp ψ = φ.toPrenexImpRight ψ
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>n : ℕ<VAR>φ ψ : L.BoundedFormula α n<VAR>hφ : φ.IsPrenex<VAR>hψ : ψ.IsPrenex<GOAL>(φ.toPrenexImp ψ).IsPrenex
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>n : ℕ<VAR>φ : L.BoundedFormula α n<GOAL>φ.toPrenex.IsPrenex
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>n : ℕ<VAR>Nonempty M<VAR>φ ψ : L.BoundedFormula α n<VAR>hφ : φ.IsQF<VAR>hψ : ψ.IsPrenex<VAR>v : α → M<VAR>xs : Fin n → M<GOAL>(φ.toPrenexImpRight ψ).Realize v xs ↔ (φ.imp ψ).Realize v xs
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>n : ℕ<VAR>Nonempty M<VAR>φ ψ : L.BoundedFormula α n<VAR>hφ : φ.IsPrenex<VAR>hψ : ψ.IsPrenex<VAR>v : α → M<VAR>xs : Fin n → M<GOAL>(φ.toPrenexImp ψ).Realize v xs ↔ (φ.imp ψ).Realize v xs
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>n : ℕ<VAR>Nonempty M<VAR>φ : L.BoundedFormula α n<VAR>v : α → M<VAR>xs : Fin n → M<GOAL>φ.toPrenex.Realize v xs ↔ φ.Realize v xs
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>n : ℕ<VAR>P : L.BoundedFormula α n → Prop<VAR>φ : L.BoundedFormula α n<VAR>h : φ.IsQF<VAR>hf : P ⊥<VAR>ha : ∀ (ψ : L.BoundedFormula α n), ψ.IsAtomic → P ψ<VAR>hsup : ∀ {φ₁ φ₂ : L.BoundedFormula α n}, P φ₁ → P φ₂ → P (φ₁ ⊔ φ₂)<VAR>hnot : ∀ {φ : L.BoundedFormula α n}, P φ → P φ.not<VAR>hse : ∀ {φ₁ φ₂ : L.BoundedFormula α n}, ∅.SemanticallyEquivalent φ₁ φ₂ → (P φ₁ ↔ P φ₂)<GOAL>P φ
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>n : ℕ<VAR>P : L.BoundedFormula α n → Prop<VAR>φ : L.BoundedFormula α n<VAR>h : φ.IsQF<VAR>hf : P ⊥<VAR>ha : ∀ (ψ : L.BoundedFormula α n), ψ.IsAtomic → P ψ<VAR>hinf : ∀ {φ₁ φ₂ : L.BoundedFormula α n}, P φ₁ → P φ₂ → P (φ₁ ⊓ φ₂)<VAR>hnot : ∀ {φ : L.BoundedFormula α n}, P φ → P φ.not<VAR>hse : ∀ {φ₁ φ₂ : L.BoundedFormula α n}, ∅.SemanticallyEquivalent φ₁ φ₂ → (P φ₁ ↔ P φ₂)<GOAL>P φ
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>n : ℕ<VAR>φ : L.BoundedFormula α n<GOAL>∅.SemanticallyEquivalent φ φ.toPrenex
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>n : ℕ<VAR>P : {m : ℕ} → L.BoundedFormula α m → Prop<VAR>φ : L.BoundedFormula α n<VAR>hqf : ∀ {m : ℕ} {ψ : L.BoundedFormula α m}, ψ.IsQF → P ψ<VAR>hall : ∀ {m : ℕ} {ψ : L.BoundedFormula α (m + 1)}, P ψ → P ψ.all<VAR>hex : ∀ {m : ℕ} {φ : L.BoundedFormula α (m + 1)}, P φ → P φ.ex<VAR>hse : ∀ {m : ℕ} {φ₁ φ₂ : L.BoundedFormula α m}, ∅.SemanticallyEquivalent φ₁ φ₂ → (P φ₁ ↔ P φ₂)<GOAL>P φ
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>n : ℕ<VAR>P : {m : ℕ} → L.BoundedFormula α m → Prop<VAR>φ : L.BoundedFormula α n<VAR>hqf : ∀ {m : ℕ} {ψ : L.BoundedFormula α m}, ψ.IsQF → P ψ<VAR>hnot : ∀ {m : ℕ} {φ : L.BoundedFormula α m}, P φ → P φ.not<VAR>hex : ∀ {m : ℕ} {φ : L.BoundedFormula α (m + 1)}, P φ → P φ.ex<VAR>hse : ∀ {m : ℕ} {φ₁ φ₂ : L.BoundedFormula α m}, ∅.SemanticallyEquivalent φ₁ φ₂ → (P φ₁ ↔ P φ₂)<GOAL>P φ
<VAR>L : FirstOrder.Language<VAR>n : ℕ<VAR>f : L.Functions n<GOAL>FirstOrder.Language.BoundedFormula.IsAtomic (FirstOrder.Language.Formula.graph f)
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>Field K<VAR>CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>hk : p ^ (k + 1) ≠ 2<GOAL>Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = (-1) ^ (φ (↑p ^ (k + 1)) / 2) * ↑↑p ^ (↑p ^ k * ((↑p - 1) * (k + 1) - 1))
<VAR>p : ℕ+<VAR>K : Type u<VAR>Field K<VAR>CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>IsCyclotomicExtension {p} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑p<VAR>hodd : p ≠ 2<GOAL>Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = (-1) ^ ((↑p - 1) / 2) * ↑↑p ^ (↑p - 2)
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>Field K<VAR>CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>IsCyclotomicExtension {p ^ k} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ k)<GOAL>Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = (-1) ^ (φ (↑p ^ k) / 2) * ↑↑p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1))
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>Field K<VAR>CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>IsCyclotomicExtension {p ^ k} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ k)<GOAL>∃ u n, Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑p ^ n
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>Field K<VAR>CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hcycl : IsCyclotomicExtension {p ^ k} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ k)<GOAL>IsIntegralClosure ↥(Algebra.adjoin ℤ {ζ}) ℤ K
<VAR>p : ℕ+<VAR>K : Type u<VAR>Field K<VAR>CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hcycl : IsCyclotomicExtension {p} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑p<GOAL>IsIntegralClosure ↥(Algebra.adjoin ℤ {ζ}) ℤ K
<VAR>p : ℕ+<VAR>k : ℕ<VAR>hp : Fact (Nat.Prime ↑p)<GOAL>IsIntegralClosure (CyclotomicRing (p ^ k) ℤ ℚ) ℤ (CyclotomicField (p ^ k) ℚ)
<VAR>p : ℕ+<VAR>hp : Fact (Nat.Prime ↑p)<GOAL>IsIntegralClosure (CyclotomicRing p ℤ ℚ) ℤ (CyclotomicField p ℚ)
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>Field K<VAR>CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>IsCyclotomicExtension {p ^ k} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ k)<VAR>a : ↥(Algebra.adjoin ℤ {ζ})<GOAL>hζ.adjoinEquivRingOfIntegers a = (IsIntegralClosure.lift ℤ (𝓞 K) K) a
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>Field K<VAR>CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>IsCyclotomicExtension {p ^ k} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ k)<VAR>a : 𝓞 K<GOAL>hζ.adjoinEquivRingOfIntegers.symm a = (IsIntegralClosure.lift ℤ (↥(Algebra.adjoin ℤ {ζ})) K) a
<VAR>K : Type u<VAR>Field K<VAR>ζ : K<VAR>k : ℕ+<VAR>hζ : IsPrimitiveRoot ζ ↑k<GOAL>↑hζ.toInteger = ζ
<VAR>K : Type u<VAR>Field K<VAR>ζ : K<VAR>NumberField K<VAR>k : ℕ+<VAR>hk : 1 < k<VAR>hζ : IsPrimitiveRoot ζ ↑k<GOAL>Finite (𝓞 K ⧸ Ideal.span {hζ.toInteger - 1})
<VAR>K : Type u<VAR>Field K<VAR>ζ : K<VAR>NumberField K<VAR>k : ℕ+<VAR>hk : 1 < k<VAR>hζ : IsPrimitiveRoot ζ ↑k<GOAL>Nat.card (𝓞 K ⧸ Ideal.span {hζ.toInteger - 1}) = ((Algebra.norm ℤ) (hζ.toInteger - 1)).natAbs
<VAR>K : Type u<VAR>Field K<VAR>ζ : K<VAR>k : ℕ+<VAR>hζ : IsPrimitiveRoot ζ ↑k<GOAL>IsPrimitiveRoot hζ.toInteger ↑k
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>Field K<VAR>CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hcycl : IsCyclotomicExtension {p ^ k} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ k)<GOAL>hζ.integralPowerBasis.gen = hζ.toInteger
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>Field K<VAR>CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hcycl : IsCyclotomicExtension {p ^ k} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ k)<GOAL>hζ.integralPowerBasis.dim = φ (↑p ^ k)
<VAR>p : ℕ+<VAR>K : Type u<VAR>Field K<VAR>CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hcycl : IsCyclotomicExtension {p} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑p<VAR>a : 𝓞 K<GOAL>hζ.adjoinEquivRingOfIntegers'.symm a = (IsIntegralClosure.lift ℤ (↥(Algebra.adjoin ℤ {ζ})) K) a
<VAR>p : ℕ+<VAR>K : Type u<VAR>Field K<VAR>CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hcycl : IsCyclotomicExtension {p} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑p<VAR>a : ↥(Algebra.adjoin ℤ {ζ})<GOAL>hζ.adjoinEquivRingOfIntegers' a = (IsIntegralClosure.lift ℤ (𝓞 K) K) a
<VAR>p : ℕ+<VAR>K : Type u<VAR>Field K<VAR>CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hcycl : IsCyclotomicExtension {p} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑p<GOAL>hζ.integralPowerBasis'.gen = hζ.toInteger
<VAR>p : ℕ+<VAR>K : Type u<VAR>Field K<VAR>CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hcycl : IsCyclotomicExtension {p} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑p<GOAL>hζ.integralPowerBasis'.dim = φ ↑p
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>Field K<VAR>CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>IsCyclotomicExtension {p ^ k} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ k)<GOAL>hζ.subOneIntegralPowerBasis.gen = ⟨ζ - 1, ⋯⟩
<VAR>p : ℕ+<VAR>K : Type u<VAR>Field K<VAR>CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hcycl : IsCyclotomicExtension {p} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑p<GOAL>hζ.subOneIntegralPowerBasis'.gen = hζ.toInteger - 1
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>Field K<VAR>CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>hodd : p ≠ 2<GOAL>Prime (hζ.toInteger - 1)
<VAR>k : ℕ<VAR>K : Type u<VAR>Field K<VAR>CharZero K<VAR>ζ : K<VAR>IsCyclotomicExtension {2 ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(2 ^ (k + 1))<GOAL>Prime (hζ.toInteger - 1)
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>Field K<VAR>CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<GOAL>Prime (hζ.toInteger - 1)
<VAR>p : ℕ+<VAR>K : Type u<VAR>Field K<VAR>CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>h : IsCyclotomicExtension {p} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑p<GOAL>Prime (hζ.toInteger - 1)
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>Field K<VAR>CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<GOAL>Prime hζ.subOneIntegralPowerBasis.gen
<VAR>p : ℕ+<VAR>K : Type u<VAR>Field K<VAR>CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>IsCyclotomicExtension {p} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑p<GOAL>Prime hζ.subOneIntegralPowerBasis'.gen
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>Field K<VAR>CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>s : ℕ<VAR>hs : s ≤ k<VAR>htwo : p ^ (k - s + 1) ≠ 2<GOAL>(Algebra.norm ℤ) (hζ.toInteger ^ ↑p ^ s - 1) = ↑↑p ^ ↑p ^ s
<VAR>k : ℕ<VAR>K : Type u<VAR>Field K<VAR>CharZero K<VAR>ζ : K<VAR>IsCyclotomicExtension {2 ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(2 ^ (k + 1))<GOAL>(Algebra.norm ℤ) (hζ.toInteger ^ 2 ^ k - 1) = (-2) ^ 2 ^ k
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>Field K<VAR>CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>s : ℕ<VAR>hs : s ≤ k<VAR>hodd : p ≠ 2<GOAL>(Algebra.norm ℤ) (hζ.toInteger ^ ↑p ^ s - 1) = ↑↑p ^ ↑p ^ s
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>Field K<VAR>CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>hodd : p ≠ 2<GOAL>(Algebra.norm ℤ) (hζ.toInteger - 1) = ↑↑p
<VAR>p : ℕ+<VAR>K : Type u<VAR>Field K<VAR>CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hcycl : IsCyclotomicExtension {p} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑p<VAR>h : p ≠ 2<GOAL>(Algebra.norm ℤ) (hζ.toInteger - 1) = ↑↑p
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>Field K<VAR>CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>htwo : p ^ (k + 1) ≠ 2<GOAL>Prime ((Algebra.norm ℤ) (hζ.toInteger - 1))
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>Field K<VAR>CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>hodd : p ≠ 2<GOAL>Prime ((Algebra.norm ℤ) (hζ.toInteger - 1))
<VAR>p : ℕ+<VAR>K : Type u<VAR>Field K<VAR>CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hcycl : IsCyclotomicExtension {p} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑p<VAR>hodd : p ≠ 2<GOAL>Prime ((Algebra.norm ℤ) (hζ.toInteger - 1))
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>Field K<VAR>CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>htwo : p ^ (k + 1) ≠ 2<GOAL>¬∃ n, ↑↑p ∣ hζ.toInteger - ↑n
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>Field K<VAR>CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>hodd : p ≠ 2<GOAL>¬∃ n, ↑↑p ∣ hζ.toInteger - ↑n
<VAR>p : ℕ+<VAR>K : Type u<VAR>Field K<VAR>CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hcycl : IsCyclotomicExtension {p} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑p<VAR>hodd : p ≠ 2<GOAL>¬∃ n, ↑↑p ∣ hζ.toInteger - ↑n
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>Field K<VAR>CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<GOAL>Finite (𝓞 K ⧸ Ideal.span {hζ.toInteger - 1})
<VAR>p : ℕ+<VAR>K : Type u<VAR>Field K<VAR>CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hcycl : IsCyclotomicExtension {p} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑p<GOAL>Finite (𝓞 K ⧸ Ideal.span {hζ.toInteger - 1})
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>Field K<VAR>CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<GOAL>hζ.toInteger - 1 ∣ ↑↑p
<VAR>p : ℕ+<VAR>K : Type u<VAR>Field K<VAR>CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hcycl : IsCyclotomicExtension {p} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑p<GOAL>hζ.toInteger - 1 ∣ ↑↑p
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>Field K<VAR>CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>hodd : p ≠ 2<GOAL>¬hζ.toInteger - 1 ∣ 2
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>Field K<VAR>CharZero K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>IsCyclotomicExtension {p ^ k} ℚ K<GOAL>NumberField.discr K = (-1) ^ (φ (↑p ^ k) / 2) * ↑↑p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1))
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>Field K<VAR>CharZero K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>IsCyclotomicExtension {p ^ (k + 1)} ℚ K<GOAL>NumberField.discr K = (-1) ^ (↑p ^ k * (↑p - 1) / 2) * ↑↑p ^ (↑p ^ k * ((↑p - 1) * (k + 1) - 1))
<VAR>p : ℕ+<VAR>K : Type u<VAR>Field K<VAR>CharZero K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>IsCyclotomicExtension {p} ℚ K<GOAL>NumberField.discr K = (-1) ^ ((↑p - 1) / 2) * ↑↑p ^ (↑p - 2)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>EuclideanDomain R<VAR>CommRing S<VAR>IsDomain S<VAR>Algebra R S<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>DecidableEq ι<VAR>Fintype ι<VAR>bS : Basis ι R S<GOAL>0 < ClassGroup.normBound abv bS
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>EuclideanDomain R<VAR>CommRing S<VAR>IsDomain S<VAR>Algebra R S<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>DecidableEq ι<VAR>Fintype ι<VAR>bS : Basis ι R S<VAR>a : S<VAR>y : ℤ<VAR>hy : ∀ (k : ι), abv ((bS.repr a) k) ≤ y<GOAL>abv ((Algebra.norm R) a) ≤ ClassGroup.normBound abv bS * y ^ Fintype.card ι
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>EuclideanDomain R<VAR>CommRing S<VAR>IsDomain S<VAR>Algebra R S<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>DecidableEq ι<VAR>Fintype ι<VAR>bS : Basis ι R S<VAR>T : Type u_6<VAR>LinearOrderedRing T<VAR>a : S<VAR>y : T<VAR>hy : ∀ (k : ι), ↑(abv ((bS.repr a) k)) < y<GOAL>↑(abv ((Algebra.norm R) a)) < ↑(ClassGroup.normBound abv bS) * y ^ Fintype.card ι
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>EuclideanDomain R<VAR>CommRing S<VAR>IsDomain S<VAR>Algebra R S<VAR>abv : AbsoluteValue R ℤ<VAR>I : ↥(Ideal S)⁰<GOAL>∃ b ∈ ↑I, b ≠ 0 ∧ ∀ c ∈ ↑I, abv ((Algebra.norm R) c) < abv ((Algebra.norm R) b) → c = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>EuclideanDomain R<VAR>CommRing S<VAR>IsDomain S<VAR>Algebra R S<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>DecidableEq ι<VAR>Fintype ι<VAR>bS : Basis ι R S<VAR>adm : abv.IsAdmissible<VAR>Infinite R<VAR>DecidableEq R<GOAL>0 ∉ ClassGroup.finsetApprox bS adm
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>EuclideanDomain R<VAR>CommRing S<VAR>IsDomain S<VAR>Algebra R S<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>DecidableEq ι<VAR>Fintype ι<VAR>bS : Basis ι R S<VAR>adm : abv.IsAdmissible<VAR>Infinite R<VAR>DecidableEq R<VAR>x : R<GOAL>x ∈ ClassGroup.finsetApprox bS adm ↔ ∃ i j, i ≠ j ∧ (ClassGroup.distinctElems bS adm) i - (ClassGroup.distinctElems bS adm) j = x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>EuclideanDomain R<VAR>CommRing S<VAR>IsDomain S<VAR>Algebra R S<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>DecidableEq ι<VAR>Fintype ι<VAR>bS : Basis ι R S<VAR>adm : abv.IsAdmissible<VAR>Infinite R<VAR>DecidableEq R<VAR>a : S<VAR>b : R<VAR>hb : b ≠ 0<GOAL>∃ q, ∃ r ∈ ClassGroup.finsetApprox bS adm, abv ((Algebra.norm R) (r • a - b • q)) < abv ((Algebra.norm R) ((algebraMap R S) b))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>L : Type u_4<VAR>EuclideanDomain R<VAR>CommRing S<VAR>IsDomain S<VAR>Field L<VAR>algRL : Algebra R L<VAR>Algebra R S<VAR>Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>DecidableEq ι<VAR>Fintype ι<VAR>bS : Basis ι R S<VAR>adm : abv.IsAdmissible<VAR>Infinite R<VAR>DecidableEq R<VAR>Algebra.IsAlgebraic R L<VAR>a : S<VAR>b : S<VAR>hb : b ≠ 0<GOAL>∃ q, ∃ r ∈ ClassGroup.finsetApprox bS adm, abv ((Algebra.norm R) (r • a - q * b)) < abv ((Algebra.norm R) b)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>EuclideanDomain R<VAR>CommRing S<VAR>IsDomain S<VAR>Algebra R S<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>DecidableEq ι<VAR>Fintype ι<VAR>bS : Basis ι R S<VAR>adm : abv.IsAdmissible<VAR>Infinite R<VAR>DecidableEq R<GOAL>(algebraMap R S) (∏ m ∈ ClassGroup.finsetApprox bS adm, m) ≠ 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>EuclideanDomain R<VAR>CommRing S<VAR>IsDomain S<VAR>Algebra R S<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>DecidableEq ι<VAR>Fintype ι<VAR>bS : Basis ι R S<VAR>adm : abv.IsAdmissible<VAR>Infinite R<VAR>DecidableEq R<VAR>J : Ideal S<VAR>h : (algebraMap R S) (∏ m ∈ ClassGroup.finsetApprox bS adm, m) ∈ J<GOAL>J ≠ ⊥
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>L : Type u_4<VAR>EuclideanDomain R<VAR>CommRing S<VAR>IsDomain S<VAR>Field L<VAR>algRL : Algebra R L<VAR>Algebra R S<VAR>Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>DecidableEq ι<VAR>Fintype ι<VAR>bS : Basis ι R S<VAR>adm : abv.IsAdmissible<VAR>Infinite R<VAR>DecidableEq R<VAR>IsDedekindDomain S<VAR>Algebra.IsAlgebraic R L<VAR>I : ↥(Ideal S)⁰<GOAL>∃ J, ClassGroup.mk0 I = ClassGroup.mk0 J ∧ (algebraMap R S) (∏ m ∈ ClassGroup.finsetApprox bS adm, m) ∈ ↑J