awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
x : K
h : IsIntegral ℤ x
u : ℤˣ
n n_1 : ℕ
hcycl : IsCyclotomicExtension {p ^ (n_1 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (n_1 + 1))
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := ⋯
hun :
  Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.subOnePowerBasis ℚ hζ))) ℚ (B := K)
      (⇑(PowerBasis.basis (IsPrimitiveRoot.subOnePowerBasis ℚ hζ)) :
        (a : Fin (IsPrimitiveRoot.subOnePowerBasis ℚ hζ).dim) → K) =
    (↑(↑u : ℤ) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) n
H :
  Membership.mem (γ := Subalgebra ℤ K) ℤ[B.gen] (HPow.hPow (α := K) ((algebraMap ℚ K : (a : ℚ) → K) (↑p : ℚ) : K) n * x)
hmin : IsEisensteinAt (minpoly ℤ B.gen) (ℤ ∙ (↑p : ℤ))
refine_1 : Membership.mem (γ := Subalgebra ℤ K) ℤ[ζ] B.gen
⊢ {B.gen} ⊆ (↑ℤ[ζ] : Set K)

Tactic:
simp only [Set.singleton_subset_iff, SetLike.mem_coe]

Premises used: Set.singleton_subset_iff, SetLike.mem_coe
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
x : K
h : IsIntegral ℤ x
u : ℤˣ
n n_1 : ℕ
hcycl : IsCyclotomicExtension {p ^ (n_1 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (n_1 + 1))
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := ⋯
hun :
  Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.subOnePowerBasis ℚ hζ))) ℚ (B := K)
      (⇑(PowerBasis.basis (IsPrimitiveRoot.subOnePowerBasis ℚ hζ)) :
        (a : Fin (IsPrimitiveRoot.subOnePowerBasis ℚ hζ).dim) → K) =
    (↑(↑u : ℤ) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) n
H :
  Membership.mem (γ := Subalgebra ℤ K) ℤ[B.gen] (HPow.hPow (α := K) ((algebraMap ℚ K : (a : ℚ) → K) (↑p : ℚ) : K) n * x)
hmin : IsEisensteinAt (minpoly ℤ B.gen) (ℤ ∙ (↑p : ℤ))
⊢ Membership.mem (γ := Subalgebra ℤ K) ℤ[ζ] B.gen

Tactic:
Subalgebra.sub_mem _ (self_mem_adjoin_singleton ℤ _) (Subalgebra.one_mem _)

Premises used: Set.Mem, Subalgebra.sub_mem, Int, Subalgebra.one_mem, Algebra.self_mem_adjoin_singleton
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
x : K
h : IsIntegral ℤ x
u : ℤˣ
n n_1 : ℕ
hcycl : IsCyclotomicExtension {p ^ (n_1 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (n_1 + 1))
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := ⋯
hun :
  Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.subOnePowerBasis ℚ hζ))) ℚ (B := K)
      (⇑(PowerBasis.basis (IsPrimitiveRoot.subOnePowerBasis ℚ hζ)) :
        (a : Fin (IsPrimitiveRoot.subOnePowerBasis ℚ hζ).dim) → K) =
    (↑(↑u : ℤ) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) n
H :
  Membership.mem (γ := Subalgebra ℤ K) ℤ[B.gen] (HPow.hPow (α := K) ((algebraMap ℚ K : (a : ℚ) → K) (↑p : ℚ) : K) n * x)
hmin : IsEisensteinAt (minpoly ℤ B.gen) (ℤ ∙ (↑p : ℤ))
⊢ Membership.mem (γ := Subalgebra ℤ K) ℤ[ζ] B.gen

Tactic:
exact Subalgebra.sub_mem _ (self_mem_adjoin_singleton ℤ _) (Subalgebra.one_mem _)

Premises used: Subalgebra.sub_mem, Int, Subalgebra.one_mem, Algebra.self_mem_adjoin_singleton
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ p
⊢ IsCyclotomicExtension {HPow.hPow (β := ℕ) p 1} ℚ K

Tactic:
rw [← pow_one p] at hζ hcycl

Premises used: pow_one
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ p
hcycl₁ : IsCyclotomicExtension {HPow.hPow (β := ℕ) p 1} ℚ K
⊢ IsPrimitiveRoot ζ (HPow.hPow (β := ℕ) p 1)

Tactic:
rw [← pow_one p] at hζ hcycl

Premises used: pow_one
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
hcycl : IsCyclotomicExtension {HPow.hPow (β := ℕ) p 1} ℚ K
hζ : IsPrimitiveRoot ζ (HPow.hPow (β := ℕ) p 1)
⊢ IsIntegralClosure ↥ℤ[ζ] ℤ K

Tactic:
isIntegralClosure_adjoin_singleton_of_prime_pow hζ

Premises used: IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton_of_prime_pow
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
hcycl : IsCyclotomicExtension {HPow.hPow (β := ℕ) p 1} ℚ K
hζ : IsPrimitiveRoot ζ (HPow.hPow (β := ℕ) p 1)
⊢ IsIntegralClosure ↥ℤ[ζ] ℤ K

Tactic:
exact isIntegralClosure_adjoin_singleton_of_prime_pow hζ

Premises used: IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton_of_prime_pow
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k : ℕ
hp : Fact (Nat.Prime p)
⊢ IsPrimitiveRoot (M := CyclotomicField (p ^ k) ℚ) (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) (p ^ k)

Tactic:
have hζ := zeta_spec (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k : ℕ
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot (M := CyclotomicField (p ^ k) ℚ) (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) (p ^ k)
⊢ IsIntegralClosure (CyclotomicRing (p ^ k) ℤ ℚ) ℤ (CyclotomicField (p ^ k) ℚ)

Tactic:
⟨IsFractionRing.injective _ _, @fun x => ⟨fun h => ⟨⟨x, ?_⟩, rfl⟩, ?_⟩⟩

Premises used: IsFractionRing.injective, IsIntegralClosure.mk, Subtype.mk, Iff.intro, Exists.intro, rfl
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k : ℕ
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot (M := CyclotomicField (p ^ k) ℚ) (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) (p ^ k)
refine_1 :
  ∀ (x : CyclotomicField (p ^ k) ℚ) (h : IsIntegral ℤ x),
    Membership.mem (γ := Subalgebra ℤ (CyclotomicField (p ^ k) ℚ))
      (adjoin ℤ {b : CyclotomicField (p ^ k) ℚ | b ^ p ^ k = 1}) x
refine_2 :
  ∀ (x : CyclotomicField (p ^ k) ℚ),
    (∃ (y : CyclotomicRing (p ^ k) ℤ ℚ),
        (algebraMap (CyclotomicRing (p ^ k) ℤ ℚ) (CyclotomicField (p ^ k) ℚ) :
              (a : CyclotomicRing (p ^ k) ℤ ℚ) → CyclotomicField (p ^ k) ℚ)
            y =
          x) →
      IsIntegral ℤ x
⊢ IsIntegralClosure (CyclotomicRing (p ^ k) ℤ ℚ) ℤ (CyclotomicField (p ^ k) ℚ)

Tactic:
refine ⟨IsFractionRing.injective _ _, @fun x => ⟨fun h => ⟨⟨x, ?_⟩, rfl⟩, ?_⟩⟩
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k : ℕ
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot (M := CyclotomicField (p ^ k) ℚ) (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) (p ^ k)
x : CyclotomicField (p ^ k) ℚ
h : IsIntegral ℤ x
refine_1 :
  ∀ (y : ↥ℤ[zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)])
    (h :
      IsIntegral ℤ (A := CyclotomicField (p ^ k) ℚ)
        ((algebraMap (↥ℤ[zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)]) (CyclotomicField (p ^ k) ℚ) :
              (a : ↥ℤ[zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)]) → CyclotomicField (p ^ k) ℚ)
            y :
          CyclotomicField (p ^ k) ℚ)),
    Membership.mem (α := CyclotomicField (p ^ k) ℚ) (γ := Subalgebra ℤ (CyclotomicField (p ^ k) ℚ))
      (adjoin ℤ {b : CyclotomicField (p ^ k) ℚ | b ^ p ^ k = 1})
      ((algebraMap (↥ℤ[zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)]) (CyclotomicField (p ^ k) ℚ) :
            (a : ↥ℤ[zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)]) → CyclotomicField (p ^ k) ℚ)
          y :
        CyclotomicField (p ^ k) ℚ)
⊢ Membership.mem (γ := Subalgebra ℤ (CyclotomicField (p ^ k) ℚ))
    (adjoin ℤ {b : CyclotomicField (p ^ k) ℚ | b ^ p ^ k = 1}) x

Tactic:
obtain ⟨y, rfl⟩ := (isIntegralClosure_adjoin_singleton_of_prime_pow hζ).isIntegral_iff.1 h

Premises used: IsIntegralClosure.isIntegral_iff, Iff.mp, rfl
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k : ℕ
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot (M := CyclotomicField (p ^ k) ℚ) (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) (p ^ k)
y : ↥ℤ[zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)]
h :
  IsIntegral ℤ (A := CyclotomicField (p ^ k) ℚ)
    ((algebraMap (↥ℤ[zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)]) (CyclotomicField (p ^ k) ℚ) :
          (a : ↥ℤ[zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)]) → CyclotomicField (p ^ k) ℚ)
        y :
      CyclotomicField (p ^ k) ℚ)
⊢ Membership.mem (α := CyclotomicField (p ^ k) ℚ) (γ := Subalgebra ℤ (CyclotomicField (p ^ k) ℚ))
    (adjoin ℤ {b : CyclotomicField (p ^ k) ℚ | b ^ p ^ k = 1})
    ((algebraMap (↥ℤ[zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)]) (CyclotomicField (p ^ k) ℚ) :
          (a : ↥ℤ[zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)]) → CyclotomicField (p ^ k) ℚ)
        y :
      CyclotomicField (p ^ k) ℚ)

Tactic:
adjoin_mono ?_ y.2

Premises used: Algebra.adjoin_mono, Subtype.property
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k : ℕ
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot (M := CyclotomicField (p ^ k) ℚ) (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) (p ^ k)
y : ↥ℤ[zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)]
h :
  IsIntegral ℤ (A := CyclotomicField (p ^ k) ℚ)
    ((algebraMap (↥ℤ[zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)]) (CyclotomicField (p ^ k) ℚ) :
          (a : ↥ℤ[zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)]) → CyclotomicField (p ^ k) ℚ)
        y :
      CyclotomicField (p ^ k) ℚ)
refine_1 :
  Subset (α := Set (CyclotomicField (p ^ k) ℚ)) {zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)}
    {b : CyclotomicField (p ^ k) ℚ | b ^ p ^ k = 1}
⊢ Membership.mem (α := CyclotomicField (p ^ k) ℚ) (γ := Subalgebra ℤ (CyclotomicField (p ^ k) ℚ))
    (adjoin ℤ {b : CyclotomicField (p ^ k) ℚ | b ^ p ^ k = 1})
    ((algebraMap (↥ℤ[zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)]) (CyclotomicField (p ^ k) ℚ) :
          (a : ↥ℤ[zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)]) → CyclotomicField (p ^ k) ℚ)
        y :
      CyclotomicField (p ^ k) ℚ)

Tactic:
refine adjoin_mono ?_ y.2

Premises used: Algebra.adjoin_mono, Subtype.property
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k : ℕ
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot (M := CyclotomicField (p ^ k) ℚ) (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) (p ^ k)
y : ↥ℤ[zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)]
h :
  IsIntegral ℤ (A := CyclotomicField (p ^ k) ℚ)
    ((algebraMap (↥ℤ[zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)]) (CyclotomicField (p ^ k) ℚ) :
          (a : ↥ℤ[zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)]) → CyclotomicField (p ^ k) ℚ)
        y :
      CyclotomicField (p ^ k) ℚ)
refine_1 : HPow.hPow (α := CyclotomicField (p ^ k) ℚ) (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) (p ^ k) = 1
⊢ Subset (α := Set (CyclotomicField (p ^ k) ℚ)) {zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)}
    {b : CyclotomicField (p ^ k) ℚ | b ^ p ^ k = 1}

Tactic:
simp only [Set.singleton_subset_iff, Set.mem_setOf_eq]

Premises used: Set.singleton_subset_iff, Set.mem_setOf_eq
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k : ℕ
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot (M := CyclotomicField (p ^ k) ℚ) (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) (p ^ k)
y : ↥ℤ[zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)]
h :
  IsIntegral ℤ (A := CyclotomicField (p ^ k) ℚ)
    ((algebraMap (↥ℤ[zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)]) (CyclotomicField (p ^ k) ℚ) :
          (a : ↥ℤ[zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)]) → CyclotomicField (p ^ k) ℚ)
        y :
      CyclotomicField (p ^ k) ℚ)
⊢ HPow.hPow (α := CyclotomicField (p ^ k) ℚ) (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) (p ^ k) = 1

Tactic:
hζ.pow_eq_one

Premises used: IsPrimitiveRoot.pow_eq_one
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k : ℕ
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot (M := CyclotomicField (p ^ k) ℚ) (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) (p ^ k)
y : ↥ℤ[zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)]
h :
  IsIntegral ℤ (A := CyclotomicField (p ^ k) ℚ)
    ((algebraMap (↥ℤ[zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)]) (CyclotomicField (p ^ k) ℚ) :
          (a : ↥ℤ[zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)]) → CyclotomicField (p ^ k) ℚ)
        y :
      CyclotomicField (p ^ k) ℚ)
⊢ HPow.hPow (α := CyclotomicField (p ^ k) ℚ) (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) (p ^ k) = 1

Tactic:
exact hζ.pow_eq_one

Premises used: IsPrimitiveRoot.pow_eq_one
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k : ℕ
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot (M := CyclotomicField (p ^ k) ℚ) (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) (p ^ k)
y : CyclotomicRing (p ^ k) ℤ ℚ
⊢ IsIntegral ℤ (A := CyclotomicField (p ^ k) ℚ)
    ((algebraMap (CyclotomicRing (p ^ k) ℤ ℚ) (CyclotomicField (p ^ k) ℚ) :
          (a : CyclotomicRing (p ^ k) ℤ ℚ) → CyclotomicField (p ^ k) ℚ)
        y :
      CyclotomicField (p ^ k) ℚ)

Tactic:
IsIntegral.algebraMap ((IsCyclotomicExtension.integral {p ^ k} ℤ _).isIntegral _)

Premises used: Algebra.IsIntegral.isIntegral, IsIntegral.algebraMap
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k : ℕ
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot (M := CyclotomicField (p ^ k) ℚ) (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) (p ^ k)
y : CyclotomicRing (p ^ k) ℤ ℚ
⊢ IsIntegral ℤ (A := CyclotomicField (p ^ k) ℚ)
    ((algebraMap (CyclotomicRing (p ^ k) ℤ ℚ) (CyclotomicField (p ^ k) ℚ) :
          (a : CyclotomicRing (p ^ k) ℤ ℚ) → CyclotomicField (p ^ k) ℚ)
        y :
      CyclotomicField (p ^ k) ℚ)

Tactic:
exact IsIntegral.algebraMap ((IsCyclotomicExtension.integral {p ^ k} ℤ _).isIntegral _)

Premises used: Algebra.IsIntegral.isIntegral, IsIntegral.algebraMap
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
rw : IsIntegralClosure (CyclotomicRing (HPow.hPow (β := ℕ) p 1) ℤ ℚ) ℤ (CyclotomicField (HPow.hPow (β := ℕ) p 1) ℚ)
⊢ IsIntegralClosure (CyclotomicRing p ℤ ℚ) ℤ (CyclotomicField p ℚ)

Tactic:
rw [← pow_one p]

Premises used: pow_one
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ IsIntegralClosure (CyclotomicRing (HPow.hPow (β := ℕ) p 1) ℤ ℚ) ℤ (CyclotomicField (HPow.hPow (β := ℕ) p 1) ℚ)

Tactic:
cyclotomicRing_isIntegralClosure_of_prime_pow

Premises used: IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure_of_prime_pow
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ IsIntegralClosure (CyclotomicRing (HPow.hPow (β := ℕ) p 1) ℤ ℚ) ℤ (CyclotomicField (HPow.hPow (β := ℕ) p 1) ℚ)

Tactic:
exact cyclotomicRing_isIntegralClosure_of_prime_pow

Premises used: IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure_of_prime_pow
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k n : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p ^ k} ℚ K
⊢ IsCyclotomicExtension.{0, u} {p ^ k} ℤ (𝓞 K)

Tactic:
let _ := (zeta_spec (p ^ k) ℚ K).adjoin_isCyclotomicExtension ℤ
  IsCyclotomicExtension.equiv _ ℤ _ (zeta_spec (p ^ k) ℚ K).adjoinEquivRingOfIntegersOfPrimePow

Premises used: Rat, Algebra.adjoin, Membership.mem, Subtype, IsPrimitiveRoot.adjoinEquivRingOfIntegersOfPrimePow, Int, HPow.hPow, IsCyclotomicExtension.equiv, IsCyclotomicExtension.zeta_spec, IsPrimitiveRoot.adjoin_isCyclotomicExtension, Singleton.singleton, IsCyclotomicExtension.zeta
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
K : Type u
inst : Field K
ζ : K
k : ℕ
inst_1 : NeZero k
hζ : IsPrimitiveRoot ζ k
⊢ (↑hζ.toInteger : K) = ζ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
K : Type u
inst : Field K
ζ : K
inst_1 : NumberField K
k : ℕ
hk : 1 < k
hζ : IsPrimitiveRoot ζ k
⊢ Finite.{u + 1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {hζ.toInteger - 1}))

Tactic:
Ideal.finiteQuotientOfFreeOfNeBot _ (fun h ↦ ?_)

Premises used: Ideal.finiteQuotientOfFreeOfNeBot
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
K : Type u
inst : Field K
ζ : K
inst_1 : NumberField K
k : ℕ
hk : 1 < k
hζ : IsPrimitiveRoot ζ k
refine : ∀ (h : Eq (α := Ideal (𝓞 K)) (Ideal.span {hζ.toInteger - 1}) ⊥), False
⊢ Finite.{u + 1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {hζ.toInteger - 1}))

Tactic:
refine Ideal.finiteQuotientOfFreeOfNeBot _ (fun h ↦ ?_)

Premises used: Ideal.finiteQuotientOfFreeOfNeBot
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
K : Type u
inst : Field K
ζ : K
inst_1 : NumberField K
k : ℕ
hk : 1 < k
hζ : IsPrimitiveRoot ζ k
h : Eq (α := Ideal (𝓞 K)) (Ideal.span {hζ.toInteger - 1}) ⊥
⊢ hζ.toInteger = 1

Tactic:
simp only [Ideal.span_singleton_eq_bot, sub_eq_zero] at h

Premises used: Ideal.span_singleton_eq_bot, sub_eq_zero
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
K : Type u
inst : Field K
ζ : K
inst_1 : NumberField K
k : ℕ
hk : 1 < k
hζ : IsPrimitiveRoot ζ k
h : hζ.toInteger = 1
⊢ False

Tactic:
hζ.ne_one hk (RingOfIntegers.ext_iff.1 h)

Premises used: Iff.mp, NumberField.RingOfIntegers.ext_iff, IsPrimitiveRoot.ne_one
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
K : Type u
inst : Field K
ζ : K
inst_1 : NumberField K
k : ℕ
hk : 1 < k
hζ : IsPrimitiveRoot ζ k
h : hζ.toInteger = 1
⊢ False

Tactic:
exact hζ.ne_one hk (RingOfIntegers.ext_iff.1 h)

Premises used: Iff.mp, NumberField.RingOfIntegers.ext_iff, IsPrimitiveRoot.ne_one
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
K : Type u
inst : Field K
ζ : K
inst_1 : NumberField K
k : ℕ
inst_2 : NeZero k
hζ : IsPrimitiveRoot ζ k
rw :
  Submodule.cardQuot.{u, u} (R := 𝓞 K) (M := 𝓞 K) (Ideal.span {hζ.toInteger - 1}) =
    Int.natAbs ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1))
rw₁ :
  (Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (Ideal.span {hζ.toInteger - 1}) =
    Int.natAbs ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1))
rw₂ rw₃ :
  Int.natAbs ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1)) =
    Int.natAbs ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1))
⊢ Nat.card.{u} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {hζ.toInteger - 1})) =
    Int.natAbs ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1))

Tactic:
rw [← Submodule.cardQuot_apply, ← Ideal.absNorm_apply, Ideal.absNorm_span_singleton]

Premises used: Ideal.absNorm_apply, Ideal.absNorm_span_singleton, Submodule.cardQuot_apply
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
K : Type u
inst : Field K
ζ : K
k : ℕ
inst_1 : NeZero k
hζ : IsPrimitiveRoot ζ k
⊢ IsPrimitiveRoot (M := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) hζ.toInteger : K) k

Tactic:
hζ
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
K : Type u
inst : Field K
ζ : K
k : ℕ
inst_1 : NeZero k
hζ : IsPrimitiveRoot ζ k
⊢ IsPrimitiveRoot (M := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) hζ.toInteger : K) k

Tactic:
exact hζ
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ k)
rw :
  (algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
      ((hζ.adjoinEquivRingOfIntegersOfPrimePow : (a : ↥ℤ[ζ]) → 𝓞 K)
          (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) ℤ[ζ] x) ζ ⋯) :
        𝓞 K) =
    (↑hζ.toInteger : K)
⊢ (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) hζ.integralPowerBasisOfPrimePow.gen = (↑hζ.toInteger : K)

Tactic:
rw [integralPowerBasisOfPrimePow, PowerBasis.map_gen, adjoin.powerBasis'_gen]

Premises used: PowerBasis.map_gen, IsPrimitiveRoot.integralPowerBasisOfPrimePow, Algebra.adjoin.powerBasis'_gen
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ k)
simp :
  (algebraMap (↥ℤ[ζ]) K : (a : ↥ℤ[ζ]) → K)
      (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) ℤ[ζ] x) ζ ⋯) =
    ζ
⊢ (algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
      ((hζ.adjoinEquivRingOfIntegersOfPrimePow : (a : ↥ℤ[ζ]) → 𝓞 K)
          (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) ℤ[ζ] x) ζ ⋯) :
        𝓞 K) =
    (↑hζ.toInteger : K)

Tactic:
simp only [adjoinEquivRingOfIntegersOfPrimePow_apply, IsIntegralClosure.algebraMap_lift]

Premises used: IsPrimitiveRoot.adjoinEquivRingOfIntegersOfPrimePow_apply, IsIntegralClosure.algebraMap_lift
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ k)
⊢ (algebraMap (↥ℤ[ζ]) K : (a : ↥ℤ[ζ]) → K)
      (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) ℤ[ζ] x) ζ ⋯) =
    ζ

Tactic:
rfl
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ k)
⊢ hζ.integralPowerBasisOfPrimePow.dim = φ (p ^ k)

Tactic:
simp [integralPowerBasisOfPrimePow, ← cyclotomic_eq_minpoly hζ (NeZero.pos _),
    natDegree_cyclotomic]

Premises used: Polynomial.natDegree_cyclotomic, IsPrimitiveRoot.integralPowerBasisOfPrimePow, NeZero.pos, Polynomial.cyclotomic_eq_minpoly
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k n : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ k)
⊢ Eq (α := Subalgebra ℤ (𝓞 K))
    ℤ[Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) (ζ - 1) ⋯] ⊤

Tactic:
hζ.integralPowerBasisOfPrimePow.adjoin_eq_top_of_gen_mem_adjoin ?_

Premises used: PowerBasis.adjoin_eq_top_of_gen_mem_adjoin
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k n : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ k)
refine :
  Membership.mem (γ := Subalgebra ℤ (𝓞 K))
    ℤ[Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) (ζ - 1) ⋯]
    hζ.integralPowerBasisOfPrimePow.gen
⊢ Eq (α := Subalgebra ℤ (𝓞 K))
    ℤ[Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) (ζ - 1) ⋯] ⊤

Tactic:
refine hζ.integralPowerBasisOfPrimePow.adjoin_eq_top_of_gen_mem_adjoin ?_

Premises used: PowerBasis.adjoin_eq_top_of_gen_mem_adjoin
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k n : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ k)
⊢ Membership.mem (γ := Subalgebra ℤ (𝓞 K))
    ℤ[Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) (ζ - 1) ⋯]
    (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) (ζ - 1) ⋯ + 1)

Tactic:
Subalgebra.add_mem _ (self_mem_adjoin_singleton ℤ _) (Subalgebra.one_mem _)

Premises used: Subalgebra.add_mem, Int, Subalgebra.one_mem, Algebra.self_mem_adjoin_singleton
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k n : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ k)
h :
  hζ.integralPowerBasisOfPrimePow.gen =
    Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) (ζ - 1) ⋯ + 1
⊢ Membership.mem (γ := Subalgebra ℤ (𝓞 K))
    ℤ[Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) (ζ - 1) ⋯]
    hζ.integralPowerBasisOfPrimePow.gen

Tactic:
convert! Subalgebra.add_mem _ (self_mem_adjoin_singleton ℤ _) (Subalgebra.one_mem _)

Premises used: Subalgebra.add_mem, Int, Subalgebra.one_mem, Algebra.self_mem_adjoin_singleton