[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
inst✝¹ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hk : p ^ (k + 1) ≠ 2
⊢ discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis =
    ↑((-1) ^ (φ ↑(p ^ (k + 1)) / 2)) * ↑↑(p ^ (↑p ^ k * ((↑p - 1) * (k + 1) - 1)))
[PROOFSTEP]
rw [← discr_prime_pow_ne_two hζ (cyclotomic.irreducible_rat (p ^ (k + 1)).pos) hk]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
inst✝¹ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hk : p ^ (k + 1) ≠ 2
⊢ discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = discr ℚ ↑(IsPrimitiveRoot.powerBasis ℚ hζ).basis
[PROOFSTEP]
exact hζ.discr_zeta_eq_discr_zeta_sub_one.symm
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
inst✝¹ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
hodd : p ≠ 2
⊢ discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑((-1) ^ ((↑p - 1) / 2)) * ↑↑(p ^ (↑p - 2))
[PROOFSTEP]
rw [← discr_odd_prime hζ (cyclotomic.irreducible_rat hp.out.pos) hodd]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
inst✝¹ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
hodd : p ≠ 2
⊢ discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = discr ℚ ↑(IsPrimitiveRoot.powerBasis ℚ hζ).basis
[PROOFSTEP]
exact hζ.discr_zeta_eq_discr_zeta_sub_one.symm
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
inst✝¹ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
⊢ discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis =
    ↑((-1) ^ (φ ↑(p ^ k) / 2)) * ↑↑(p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1)))
[PROOFSTEP]
rw [← discr_prime_pow hζ (cyclotomic.irreducible_rat (p ^ k).pos)]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
inst✝¹ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
⊢ discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = discr ℚ ↑(IsPrimitiveRoot.powerBasis ℚ hζ).basis
[PROOFSTEP]
exact hζ.discr_zeta_eq_discr_zeta_sub_one.symm
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
inst✝¹ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
⊢ ∃ u n, discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
[PROOFSTEP]
rw [hζ.discr_zeta_eq_discr_zeta_sub_one.symm]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
inst✝¹ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
⊢ ∃ u n, discr ℚ ↑(IsPrimitiveRoot.powerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
[PROOFSTEP]
exact discr_prime_pow_eq_unit_mul_pow hζ (cyclotomic.irreducible_rat (p ^ k).pos)
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
⊢ IsIntegralClosure { x // x ∈ adjoin ℤ {ζ} } ℤ K
[PROOFSTEP]
refine' ⟨Subtype.val_injective, @fun x => ⟨fun h => ⟨⟨x, _⟩, rfl⟩, _⟩⟩
[GOAL]
case refine'_1
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
x : K
h : IsIntegral ℤ x
⊢ x ∈ adjoin ℤ {ζ}
case refine'_2
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
x : K
⊢ (∃ y, ↑(algebraMap { x // x ∈ adjoin ℤ {ζ} } K) y = x) → IsIntegral ℤ x
[PROOFSTEP]
swap
[GOAL]
case refine'_2
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
x : K
⊢ (∃ y, ↑(algebraMap { x // x ∈ adjoin ℤ {ζ} } K) y = x) → IsIntegral ℤ x
[PROOFSTEP]
rintro ⟨y, rfl⟩
[GOAL]
case refine'_2.intro
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
y : { x // x ∈ adjoin ℤ {ζ} }
⊢ IsIntegral ℤ (↑(algebraMap { x // x ∈ adjoin ℤ {ζ} } K) y)
[PROOFSTEP]
exact
  IsIntegral.algebraMap (le_integralClosure_iff_isIntegral.1 (adjoin_le_integralClosure (hζ.isIntegral (p ^ k).pos)) _)
[GOAL]
case refine'_1
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
x : K
h : IsIntegral ℤ x
⊢ x ∈ adjoin ℤ {ζ}
[PROOFSTEP]
let B := hζ.subOnePowerBasis ℚ
[GOAL]
case refine'_1
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
x : K
h : IsIntegral ℤ x
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
⊢ x ∈ adjoin ℤ {ζ}
[PROOFSTEP]
have hint : IsIntegral ℤ B.gen := isIntegral_sub (hζ.isIntegral (p ^ k).pos) isIntegral_one
[GOAL]
case refine'_1
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
x : K
h : IsIntegral ℤ x
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
⊢ x ∈ adjoin ℤ {ζ}
[PROOFSTEP]
letI := IsCyclotomicExtension.finiteDimensional {p ^ k} ℚ K
[GOAL]
case refine'_1
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
x : K
h : IsIntegral ℤ x
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := finiteDimensional {p ^ k} ℚ K
⊢ x ∈ adjoin ℤ {ζ}
[PROOFSTEP]
have H := discr_mul_isIntegral_mem_adjoin ℚ hint h
[GOAL]
case refine'_1
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
x : K
h : IsIntegral ℤ x
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := finiteDimensional {p ^ k} ℚ K
H : discr ℚ ↑B.basis • x ∈ adjoin ℤ {B.gen}
⊢ x ∈ adjoin ℤ {ζ}
[PROOFSTEP]
obtain ⟨u, n, hun⟩ := discr_prime_pow_eq_unit_mul_pow' hζ
[GOAL]
case refine'_1.intro.intro
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
x : K
h : IsIntegral ℤ x
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := finiteDimensional {p ^ k} ℚ K
H : discr ℚ ↑B.basis • x ∈ adjoin ℤ {B.gen}
u : ℤˣ
n : ℕ
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
⊢ x ∈ adjoin ℤ {ζ}
[PROOFSTEP]
rw [hun] at H 
[GOAL]
case refine'_1.intro.intro
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
x : K
h : IsIntegral ℤ x
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := finiteDimensional {p ^ k} ℚ K
u : ℤˣ
n : ℕ
H : (↑↑u * ↑↑(p ^ n)) • x ∈ adjoin ℤ {B.gen}
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
⊢ x ∈ adjoin ℤ {ζ}
[PROOFSTEP]
replace H := Subalgebra.smul_mem _ H u.inv
[GOAL]
case refine'_1.intro.intro
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
x : K
h : IsIntegral ℤ x
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := finiteDimensional {p ^ k} ℚ K
u : ℤˣ
n : ℕ
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
H : u.inv • (↑↑u * ↑↑(p ^ n)) • x ∈ adjoin ℤ {B.gen}
⊢ x ∈ adjoin ℤ {ζ}
[PROOFSTEP]
rw [← smul_assoc, ← smul_mul_assoc, Units.inv_eq_val_inv, zsmul_eq_mul, ← Int.cast_mul, Units.inv_mul, Int.cast_one,
  one_mul, PNat.pow_coe, Nat.cast_pow, smul_def, map_pow] at H 
[GOAL]
case refine'_1.intro.intro
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
x : K
h : IsIntegral ℤ x
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := finiteDimensional {p ^ k} ℚ K
u : ℤˣ
n : ℕ
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
H✝ : u.inv • (↑↑u * ↑↑(p ^ n)) • x ∈ adjoin ℤ {B.gen}
H : ↑(algebraMap ℚ K) ↑↑p ^ n * x ∈ adjoin ℤ {B.gen}
⊢ x ∈ adjoin ℤ {ζ}
[PROOFSTEP]
cases k
[GOAL]
case refine'_1.intro.intro.zero
p : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
x : K
h : IsIntegral ℤ x
u : ℤˣ
n : ℕ
hcycl : IsCyclotomicExtension {p ^ Nat.zero} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.zero)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := finiteDimensional {p ^ Nat.zero} ℚ K
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
H✝ : u.inv • (↑↑u * ↑↑(p ^ n)) • x ∈ adjoin ℤ {B.gen}
H : ↑(algebraMap ℚ K) ↑↑p ^ n * x ∈ adjoin ℤ {B.gen}
⊢ x ∈ adjoin ℤ {ζ}
[PROOFSTEP]
haveI : IsCyclotomicExtension {1} ℚ K := by simpa using hcycl
[GOAL]
p : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
x : K
h : IsIntegral ℤ x
u : ℤˣ
n : ℕ
hcycl : IsCyclotomicExtension {p ^ Nat.zero} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.zero)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := finiteDimensional {p ^ Nat.zero} ℚ K
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
H✝ : u.inv • (↑↑u * ↑↑(p ^ n)) • x ∈ adjoin ℤ {B.gen}
H : ↑(algebraMap ℚ K) ↑↑p ^ n * x ∈ adjoin ℤ {B.gen}
⊢ IsCyclotomicExtension {1} ℚ K
[PROOFSTEP]
simpa using hcycl
[GOAL]
case refine'_1.intro.intro.zero
p : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
x : K
h : IsIntegral ℤ x
u : ℤˣ
n : ℕ
hcycl : IsCyclotomicExtension {p ^ Nat.zero} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.zero)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this✝ : FiniteDimensional ℚ K := finiteDimensional {p ^ Nat.zero} ℚ K
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
H✝ : u.inv • (↑↑u * ↑↑(p ^ n)) • x ∈ adjoin ℤ {B.gen}
H : ↑(algebraMap ℚ K) ↑↑p ^ n * x ∈ adjoin ℤ {B.gen}
this : IsCyclotomicExtension {1} ℚ K
⊢ x ∈ adjoin ℤ {ζ}
[PROOFSTEP]
have : x ∈ (⊥ : Subalgebra ℚ K) := by
  rw [singleton_one ℚ K]
  exact mem_top
[GOAL]
p : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
x : K
h : IsIntegral ℤ x
u : ℤˣ
n : ℕ
hcycl : IsCyclotomicExtension {p ^ Nat.zero} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.zero)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this✝ : FiniteDimensional ℚ K := finiteDimensional {p ^ Nat.zero} ℚ K
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
H✝ : u.inv • (↑↑u * ↑↑(p ^ n)) • x ∈ adjoin ℤ {B.gen}
H : ↑(algebraMap ℚ K) ↑↑p ^ n * x ∈ adjoin ℤ {B.gen}
this : IsCyclotomicExtension {1} ℚ K
⊢ x ∈ ⊥
[PROOFSTEP]
rw [singleton_one ℚ K]
[GOAL]
p : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
x : K
h : IsIntegral ℤ x
u : ℤˣ
n : ℕ
hcycl : IsCyclotomicExtension {p ^ Nat.zero} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.zero)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this✝ : FiniteDimensional ℚ K := finiteDimensional {p ^ Nat.zero} ℚ K
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
H✝ : u.inv • (↑↑u * ↑↑(p ^ n)) • x ∈ adjoin ℤ {B.gen}
H : ↑(algebraMap ℚ K) ↑↑p ^ n * x ∈ adjoin ℤ {B.gen}
this : IsCyclotomicExtension {1} ℚ K
⊢ x ∈ ⊤
[PROOFSTEP]
exact mem_top
[GOAL]
case refine'_1.intro.intro.zero
p : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
x : K
h : IsIntegral ℤ x
u : ℤˣ
n : ℕ
hcycl : IsCyclotomicExtension {p ^ Nat.zero} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.zero)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this✝¹ : FiniteDimensional ℚ K := finiteDimensional {p ^ Nat.zero} ℚ K
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
H✝ : u.inv • (↑↑u * ↑↑(p ^ n)) • x ∈ adjoin ℤ {B.gen}
H : ↑(algebraMap ℚ K) ↑↑p ^ n * x ∈ adjoin ℤ {B.gen}
this✝ : IsCyclotomicExtension {1} ℚ K
this : x ∈ ⊥
⊢ x ∈ adjoin ℤ {ζ}
[PROOFSTEP]
obtain ⟨y, rfl⟩ := mem_bot.1 this
[GOAL]
case refine'_1.intro.intro.zero.intro
p : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
u : ℤˣ
n : ℕ
hcycl : IsCyclotomicExtension {p ^ Nat.zero} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.zero)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this✝¹ : FiniteDimensional ℚ K := finiteDimensional {p ^ Nat.zero} ℚ K
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
this✝ : IsCyclotomicExtension {1} ℚ K
y : ℚ
h : IsIntegral ℤ (↑(algebraMap ℚ K) y)
H✝ : u.inv • (↑↑u * ↑↑(p ^ n)) • ↑(algebraMap ℚ K) y ∈ adjoin ℤ {B.gen}
H : ↑(algebraMap ℚ K) ↑↑p ^ n * ↑(algebraMap ℚ K) y ∈ adjoin ℤ {B.gen}
this : ↑(algebraMap ℚ K) y ∈ ⊥
⊢ ↑(algebraMap ℚ K) y ∈ adjoin ℤ {ζ}
[PROOFSTEP]
replace h := (isIntegral_algebraMap_iff (algebraMap ℚ K).injective).1 h
[GOAL]
case refine'_1.intro.intro.zero.intro
p : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
u : ℤˣ
n : ℕ
hcycl : IsCyclotomicExtension {p ^ Nat.zero} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.zero)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this✝¹ : FiniteDimensional ℚ K := finiteDimensional {p ^ Nat.zero} ℚ K
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
this✝ : IsCyclotomicExtension {1} ℚ K
y : ℚ
H✝ : u.inv • (↑↑u * ↑↑(p ^ n)) • ↑(algebraMap ℚ K) y ∈ adjoin ℤ {B.gen}
H : ↑(algebraMap ℚ K) ↑↑p ^ n * ↑(algebraMap ℚ K) y ∈ adjoin ℤ {B.gen}
this : ↑(algebraMap ℚ K) y ∈ ⊥
h : IsIntegral ℤ y
⊢ ↑(algebraMap ℚ K) y ∈ adjoin ℤ {ζ}
[PROOFSTEP]
obtain ⟨z, hz⟩ := IsIntegrallyClosed.isIntegral_iff.1 h
[GOAL]
case refine'_1.intro.intro.zero.intro.intro
p : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
u : ℤˣ
n : ℕ
hcycl : IsCyclotomicExtension {p ^ Nat.zero} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.zero)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this✝¹ : FiniteDimensional ℚ K := finiteDimensional {p ^ Nat.zero} ℚ K
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
this✝ : IsCyclotomicExtension {1} ℚ K
y : ℚ
H✝ : u.inv • (↑↑u * ↑↑(p ^ n)) • ↑(algebraMap ℚ K) y ∈ adjoin ℤ {B.gen}
H : ↑(algebraMap ℚ K) ↑↑p ^ n * ↑(algebraMap ℚ K) y ∈ adjoin ℤ {B.gen}
this : ↑(algebraMap ℚ K) y ∈ ⊥
h : IsIntegral ℤ y
z : ℤ
hz : ↑(algebraMap ℤ ℚ) z = y
⊢ ↑(algebraMap ℚ K) y ∈ adjoin ℤ {ζ}
[PROOFSTEP]
rw [← hz, ← IsScalarTower.algebraMap_apply]
[GOAL]
case refine'_1.intro.intro.zero.intro.intro
p : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
u : ℤˣ
n : ℕ
hcycl : IsCyclotomicExtension {p ^ Nat.zero} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.zero)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this✝¹ : FiniteDimensional ℚ K := finiteDimensional {p ^ Nat.zero} ℚ K
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
this✝ : IsCyclotomicExtension {1} ℚ K
y : ℚ
H✝ : u.inv • (↑↑u * ↑↑(p ^ n)) • ↑(algebraMap ℚ K) y ∈ adjoin ℤ {B.gen}
H : ↑(algebraMap ℚ K) ↑↑p ^ n * ↑(algebraMap ℚ K) y ∈ adjoin ℤ {B.gen}
this : ↑(algebraMap ℚ K) y ∈ ⊥
h : IsIntegral ℤ y
z : ℤ
hz : ↑(algebraMap ℤ ℚ) z = y
⊢ ↑(algebraMap ℤ K) z ∈ adjoin ℤ {ζ}
[PROOFSTEP]
exact Subalgebra.algebraMap_mem _ _
[GOAL]
case refine'_1.intro.intro.succ
p : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
x : K
h : IsIntegral ℤ x
u : ℤˣ
n n✝ : ℕ
hcycl : IsCyclotomicExtension {p ^ Nat.succ n✝} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.succ n✝)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := finiteDimensional {p ^ Nat.succ n✝} ℚ K
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
H✝ : u.inv • (↑↑u * ↑↑(p ^ n)) • x ∈ adjoin ℤ {B.gen}
H : ↑(algebraMap ℚ K) ↑↑p ^ n * x ∈ adjoin ℤ {B.gen}
⊢ x ∈ adjoin ℤ {ζ}
[PROOFSTEP]
have hmin : (minpoly ℤ B.gen).IsEisensteinAt (Submodule.span ℤ {((p : ℕ) : ℤ)}) :=
  by
  have h₁ := minpoly.isIntegrallyClosed_eq_field_fractions' ℚ hint
  have h₂ := hζ.minpoly_sub_one_eq_cyclotomic_comp (cyclotomic.irreducible_rat (p ^ _).pos)
  rw [IsPrimitiveRoot.subOnePowerBasis_gen] at h₁ 
  rw [h₁, ← map_cyclotomic_int, show Int.castRingHom ℚ = algebraMap ℤ ℚ by rfl,
    show X + 1 = map (algebraMap ℤ ℚ) (X + 1) by simp, ← map_comp] at h₂ 
  haveI : CharZero ℚ := StrictOrderedSemiring.to_charZero
  rw [IsPrimitiveRoot.subOnePowerBasis_gen, map_injective (algebraMap ℤ ℚ) (algebraMap ℤ ℚ).injective_int h₂]
  exact cyclotomic_prime_pow_comp_X_add_one_isEisensteinAt p _
[GOAL]
p : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
x : K
h : IsIntegral ℤ x
u : ℤˣ
n n✝ : ℕ
hcycl : IsCyclotomicExtension {p ^ Nat.succ n✝} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.succ n✝)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := finiteDimensional {p ^ Nat.succ n✝} ℚ K
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
H✝ : u.inv • (↑↑u * ↑↑(p ^ n)) • x ∈ adjoin ℤ {B.gen}
H : ↑(algebraMap ℚ K) ↑↑p ^ n * x ∈ adjoin ℤ {B.gen}
⊢ IsEisensteinAt (minpoly ℤ B.gen) (Submodule.span ℤ {↑↑p})
[PROOFSTEP]
have h₁ := minpoly.isIntegrallyClosed_eq_field_fractions' ℚ hint
[GOAL]
p : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
x : K
h : IsIntegral ℤ x
u : ℤˣ
n n✝ : ℕ
hcycl : IsCyclotomicExtension {p ^ Nat.succ n✝} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.succ n✝)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := finiteDimensional {p ^ Nat.succ n✝} ℚ K
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
H✝ : u.inv • (↑↑u * ↑↑(p ^ n)) • x ∈ adjoin ℤ {B.gen}
H : ↑(algebraMap ℚ K) ↑↑p ^ n * x ∈ adjoin ℤ {B.gen}
h₁ : minpoly ℚ B.gen = map (algebraMap ℤ ℚ) (minpoly ℤ B.gen)
⊢ IsEisensteinAt (minpoly ℤ B.gen) (Submodule.span ℤ {↑↑p})
[PROOFSTEP]
have h₂ := hζ.minpoly_sub_one_eq_cyclotomic_comp (cyclotomic.irreducible_rat (p ^ _).pos)
[GOAL]
p : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
x : K
h : IsIntegral ℤ x
u : ℤˣ
n n✝ : ℕ
hcycl : IsCyclotomicExtension {p ^ Nat.succ n✝} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.succ n✝)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := finiteDimensional {p ^ Nat.succ n✝} ℚ K
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
H✝ : u.inv • (↑↑u * ↑↑(p ^ n)) • x ∈ adjoin ℤ {B.gen}
H : ↑(algebraMap ℚ K) ↑↑p ^ n * x ∈ adjoin ℤ {B.gen}
h₁ : minpoly ℚ B.gen = map (algebraMap ℤ ℚ) (minpoly ℤ B.gen)
h₂ : minpoly ℚ (ζ - 1) = comp (cyclotomic ↑(p ^ Nat.succ n✝) ℚ) (X + 1)
⊢ IsEisensteinAt (minpoly ℤ B.gen) (Submodule.span ℤ {↑↑p})
[PROOFSTEP]
rw [IsPrimitiveRoot.subOnePowerBasis_gen] at h₁ 
[GOAL]
p : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
x : K
h : IsIntegral ℤ x
u : ℤˣ
n n✝ : ℕ
hcycl : IsCyclotomicExtension {p ^ Nat.succ n✝} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.succ n✝)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := finiteDimensional {p ^ Nat.succ n✝} ℚ K
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
H✝ : u.inv • (↑↑u * ↑↑(p ^ n)) • x ∈ adjoin ℤ {B.gen}
H : ↑(algebraMap ℚ K) ↑↑p ^ n * x ∈ adjoin ℤ {B.gen}
h₁ : minpoly ℚ (ζ - 1) = map (algebraMap ℤ ℚ) (minpoly ℤ (ζ - 1))
h₂ : minpoly ℚ (ζ - 1) = comp (cyclotomic ↑(p ^ Nat.succ n✝) ℚ) (X + 1)
⊢ IsEisensteinAt (minpoly ℤ B.gen) (Submodule.span ℤ {↑↑p})
[PROOFSTEP]
rw [h₁, ← map_cyclotomic_int, show Int.castRingHom ℚ = algebraMap ℤ ℚ by rfl,
  show X + 1 = map (algebraMap ℤ ℚ) (X + 1) by simp, ← map_comp] at h₂ 
[GOAL]
p : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
x : K
h : IsIntegral ℤ x
u : ℤˣ
n n✝ : ℕ
hcycl : IsCyclotomicExtension {p ^ Nat.succ n✝} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.succ n✝)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := finiteDimensional {p ^ Nat.succ n✝} ℚ K
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
H✝ : u.inv • (↑↑u * ↑↑(p ^ n)) • x ∈ adjoin ℤ {B.gen}
H : ↑(algebraMap ℚ K) ↑↑p ^ n * x ∈ adjoin ℤ {B.gen}
h₁ : minpoly ℚ (ζ - 1) = map (algebraMap ℤ ℚ) (minpoly ℤ (ζ - 1))
h₂ : map (algebraMap ℤ ℚ) (minpoly ℤ (ζ - 1)) = comp (map (Int.castRingHom ℚ) (cyclotomic ↑(p ^ Nat.succ n✝) ℤ)) (X + 1)
⊢ Int.castRingHom ℚ = algebraMap ℤ ℚ
[PROOFSTEP]
rfl
[GOAL]
p : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
x : K
h : IsIntegral ℤ x
u : ℤˣ
n n✝ : ℕ
hcycl : IsCyclotomicExtension {p ^ Nat.succ n✝} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.succ n✝)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := finiteDimensional {p ^ Nat.succ n✝} ℚ K
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
H✝ : u.inv • (↑↑u * ↑↑(p ^ n)) • x ∈ adjoin ℤ {B.gen}
H : ↑(algebraMap ℚ K) ↑↑p ^ n * x ∈ adjoin ℤ {B.gen}
h₁ : minpoly ℚ (ζ - 1) = map (algebraMap ℤ ℚ) (minpoly ℤ (ζ - 1))
h₂ : map (algebraMap ℤ ℚ) (minpoly ℤ (ζ - 1)) = comp (map (algebraMap ℤ ℚ) (cyclotomic ↑(p ^ Nat.succ n✝) ℤ)) (X + 1)
⊢ X + 1 = map (algebraMap ℤ ℚ) (X + 1)
[PROOFSTEP]
simp
[GOAL]
p : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
x : K
h : IsIntegral ℤ x
u : ℤˣ
n n✝ : ℕ
hcycl : IsCyclotomicExtension {p ^ Nat.succ n✝} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.succ n✝)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := finiteDimensional {p ^ Nat.succ n✝} ℚ K
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
H✝ : u.inv • (↑↑u * ↑↑(p ^ n)) • x ∈ adjoin ℤ {B.gen}
H : ↑(algebraMap ℚ K) ↑↑p ^ n * x ∈ adjoin ℤ {B.gen}
h₁ : minpoly ℚ (ζ - 1) = map (algebraMap ℤ ℚ) (minpoly ℤ (ζ - 1))
h₂ : map (algebraMap ℤ ℚ) (minpoly ℤ (ζ - 1)) = map (algebraMap ℤ ℚ) (comp (cyclotomic ↑(p ^ Nat.succ n✝) ℤ) (X + 1))
⊢ IsEisensteinAt (minpoly ℤ B.gen) (Submodule.span ℤ {↑↑p})
[PROOFSTEP]
haveI : CharZero ℚ := StrictOrderedSemiring.to_charZero
[GOAL]
p : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
x : K
h : IsIntegral ℤ x
u : ℤˣ
n n✝ : ℕ
hcycl : IsCyclotomicExtension {p ^ Nat.succ n✝} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.succ n✝)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this✝ : FiniteDimensional ℚ K := finiteDimensional {p ^ Nat.succ n✝} ℚ K
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
H✝ : u.inv • (↑↑u * ↑↑(p ^ n)) • x ∈ adjoin ℤ {B.gen}
H : ↑(algebraMap ℚ K) ↑↑p ^ n * x ∈ adjoin ℤ {B.gen}
h₁ : minpoly ℚ (ζ - 1) = map (algebraMap ℤ ℚ) (minpoly ℤ (ζ - 1))
h₂ : map (algebraMap ℤ ℚ) (minpoly ℤ (ζ - 1)) = map (algebraMap ℤ ℚ) (comp (cyclotomic ↑(p ^ Nat.succ n✝) ℤ) (X + 1))
this : CharZero ℚ
⊢ IsEisensteinAt (minpoly ℤ B.gen) (Submodule.span ℤ {↑↑p})
[PROOFSTEP]
rw [IsPrimitiveRoot.subOnePowerBasis_gen, map_injective (algebraMap ℤ ℚ) (algebraMap ℤ ℚ).injective_int h₂]
[GOAL]
p : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
x : K
h : IsIntegral ℤ x
u : ℤˣ
n n✝ : ℕ
hcycl : IsCyclotomicExtension {p ^ Nat.succ n✝} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.succ n✝)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this✝ : FiniteDimensional ℚ K := finiteDimensional {p ^ Nat.succ n✝} ℚ K
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
H✝ : u.inv • (↑↑u * ↑↑(p ^ n)) • x ∈ adjoin ℤ {B.gen}
H : ↑(algebraMap ℚ K) ↑↑p ^ n * x ∈ adjoin ℤ {B.gen}
h₁ : minpoly ℚ (ζ - 1) = map (algebraMap ℤ ℚ) (minpoly ℤ (ζ - 1))
h₂ : map (algebraMap ℤ ℚ) (minpoly ℤ (ζ - 1)) = map (algebraMap ℤ ℚ) (comp (cyclotomic ↑(p ^ Nat.succ n✝) ℤ) (X + 1))
this : CharZero ℚ
⊢ IsEisensteinAt (comp (cyclotomic ↑(p ^ Nat.succ n✝) ℤ) (X + 1)) (Submodule.span ℤ {↑↑p})
[PROOFSTEP]
exact cyclotomic_prime_pow_comp_X_add_one_isEisensteinAt p _
[GOAL]
case refine'_1.intro.intro.succ
p : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
x : K
h : IsIntegral ℤ x
u : ℤˣ
n n✝ : ℕ
hcycl : IsCyclotomicExtension {p ^ Nat.succ n✝} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.succ n✝)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := finiteDimensional {p ^ Nat.succ n✝} ℚ K
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
H✝ : u.inv • (↑↑u * ↑↑(p ^ n)) • x ∈ adjoin ℤ {B.gen}
H : ↑(algebraMap ℚ K) ↑↑p ^ n * x ∈ adjoin ℤ {B.gen}
hmin : IsEisensteinAt (minpoly ℤ B.gen) (Submodule.span ℤ {↑↑p})
⊢ x ∈ adjoin ℤ {ζ}
[PROOFSTEP]
refine'
  adjoin_le _
    (mem_adjoin_of_smul_prime_pow_smul_of_minpoly_isEisensteinAt (n := n) (Nat.prime_iff_prime_int.1 hp.out) hint h
      (by simpa using H) hmin)
[GOAL]
p : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
x : K
h : IsIntegral ℤ x
u : ℤˣ
n n✝ : ℕ
hcycl : IsCyclotomicExtension {p ^ Nat.succ n✝} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.succ n✝)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := finiteDimensional {p ^ Nat.succ n✝} ℚ K
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
H✝ : u.inv • (↑↑u * ↑↑(p ^ n)) • x ∈ adjoin ℤ {B.gen}
H : ↑(algebraMap ℚ K) ↑↑p ^ n * x ∈ adjoin ℤ {B.gen}
hmin : IsEisensteinAt (minpoly ℤ B.gen) (Submodule.span ℤ {↑↑p})
⊢ ↑↑p ^ n • x ∈ adjoin ℤ {B.gen}
[PROOFSTEP]
simpa using H
[GOAL]
case refine'_1.intro.intro.succ
p : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
x : K
h : IsIntegral ℤ x
u : ℤˣ
n n✝ : ℕ
hcycl : IsCyclotomicExtension {p ^ Nat.succ n✝} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.succ n✝)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := finiteDimensional {p ^ Nat.succ n✝} ℚ K
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
H✝ : u.inv • (↑↑u * ↑↑(p ^ n)) • x ∈ adjoin ℤ {B.gen}
H : ↑(algebraMap ℚ K) ↑↑p ^ n * x ∈ adjoin ℤ {B.gen}
hmin : IsEisensteinAt (minpoly ℤ B.gen) (Submodule.span ℤ {↑↑p})
⊢ {B.gen} ⊆ ↑(adjoin ℤ {ζ})
[PROOFSTEP]
simp only [Set.singleton_subset_iff, SetLike.mem_coe]
[GOAL]
case refine'_1.intro.intro.succ
p : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
x : K
h : IsIntegral ℤ x
u : ℤˣ
n n✝ : ℕ
hcycl : IsCyclotomicExtension {p ^ Nat.succ n✝} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.succ n✝)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := finiteDimensional {p ^ Nat.succ n✝} ℚ K
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
H✝ : u.inv • (↑↑u * ↑↑(p ^ n)) • x ∈ adjoin ℤ {B.gen}
H : ↑(algebraMap ℚ K) ↑↑p ^ n * x ∈ adjoin ℤ {B.gen}
hmin : IsEisensteinAt (minpoly ℤ B.gen) (Submodule.span ℤ {↑↑p})
⊢ (IsPrimitiveRoot.subOnePowerBasis ℚ hζ).gen ∈ adjoin ℤ {ζ}
[PROOFSTEP]
exact Subalgebra.sub_mem _ (self_mem_adjoin_singleton ℤ _) (Subalgebra.one_mem _)
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ IsIntegralClosure { x // x ∈ adjoin ℤ {ζ} } ℤ K
[PROOFSTEP]
rw [← pow_one p] at hζ hcycl 
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ 1} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ 1)
⊢ IsIntegralClosure { x // x ∈ adjoin ℤ {ζ} } ℤ K
[PROOFSTEP]
exact isIntegralClosure_adjoin_singleton_of_prime_pow hζ
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
⊢ IsIntegralClosure (CyclotomicRing (p ^ k) ℤ ℚ) ℤ (CyclotomicField (p ^ k) ℚ)
[PROOFSTEP]
haveI : CharZero ℚ := StrictOrderedSemiring.to_charZero
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
this : CharZero ℚ
⊢ IsIntegralClosure (CyclotomicRing (p ^ k) ℤ ℚ) ℤ (CyclotomicField (p ^ k) ℚ)
[PROOFSTEP]
have hζ := zeta_spec (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
this : CharZero ℚ
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) ↑(p ^ k)
⊢ IsIntegralClosure (CyclotomicRing (p ^ k) ℤ ℚ) ℤ (CyclotomicField (p ^ k) ℚ)
[PROOFSTEP]
refine'
  ⟨IsFractionRing.injective _ _, @fun x => ⟨fun h => ⟨⟨x, _⟩, rfl⟩, _⟩⟩
    -- Porting note: having `.isIntegral_iff` inside the definition of `this` causes an error.
[GOAL]
case refine'_1
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
this : CharZero ℚ
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) ↑(p ^ k)
x : CyclotomicField (p ^ k) ℚ
h : IsIntegral ℤ x
⊢ x ∈ adjoin ℤ {b | b ^ ↑(p ^ k) = 1}
[PROOFSTEP]
have := (isIntegralClosure_adjoin_singleton_of_prime_pow hζ)
[GOAL]
case refine'_1
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
this✝ : CharZero ℚ
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) ↑(p ^ k)
x : CyclotomicField (p ^ k) ℚ
h : IsIntegral ℤ x
this :
  IsIntegralClosure { x // x ∈ adjoin ℤ {zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)} } ℤ (CyclotomicField (p ^ k) ℚ)
⊢ x ∈ adjoin ℤ {b | b ^ ↑(p ^ k) = 1}
[PROOFSTEP]
obtain ⟨y, rfl⟩ := this.isIntegral_iff.1 h
[GOAL]
case refine'_1.intro
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
this✝ : CharZero ℚ
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) ↑(p ^ k)
this :
  IsIntegralClosure { x // x ∈ adjoin ℤ {zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)} } ℤ (CyclotomicField (p ^ k) ℚ)
y : { x // x ∈ adjoin ℤ {zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)} }
h :
  IsIntegral ℤ
    (↑(algebraMap { x // x ∈ adjoin ℤ {zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)} } (CyclotomicField (p ^ k) ℚ)) y)
⊢ ↑(algebraMap { x // x ∈ adjoin ℤ {zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)} } (CyclotomicField (p ^ k) ℚ)) y ∈
    adjoin ℤ {b | b ^ ↑(p ^ k) = 1}
[PROOFSTEP]
refine' adjoin_mono _ y.2
[GOAL]
case refine'_1.intro
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
this✝ : CharZero ℚ
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) ↑(p ^ k)
this :
  IsIntegralClosure { x // x ∈ adjoin ℤ {zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)} } ℤ (CyclotomicField (p ^ k) ℚ)
y : { x // x ∈ adjoin ℤ {zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)} }
h :
  IsIntegral ℤ
    (↑(algebraMap { x // x ∈ adjoin ℤ {zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)} } (CyclotomicField (p ^ k) ℚ)) y)
⊢ {zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)} ⊆ {b | b ^ ↑(p ^ k) = 1}
[PROOFSTEP]
simp only [PNat.pow_coe, Set.singleton_subset_iff, Set.mem_setOf_eq]
[GOAL]
case refine'_1.intro
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
this✝ : CharZero ℚ
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) ↑(p ^ k)
this :
  IsIntegralClosure { x // x ∈ adjoin ℤ {zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)} } ℤ (CyclotomicField (p ^ k) ℚ)
y : { x // x ∈ adjoin ℤ {zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)} }
h :
  IsIntegral ℤ
    (↑(algebraMap { x // x ∈ adjoin ℤ {zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)} } (CyclotomicField (p ^ k) ℚ)) y)
⊢ zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ) ^ ↑p ^ k = 1
[PROOFSTEP]
exact hζ.pow_eq_one
[GOAL]
case refine'_2
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
this : CharZero ℚ
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) ↑(p ^ k)
x : CyclotomicField (p ^ k) ℚ
⊢ (∃ y, ↑(algebraMap (CyclotomicRing (p ^ k) ℤ ℚ) (CyclotomicField (p ^ k) ℚ)) y = x) → IsIntegral ℤ x
[PROOFSTEP]
rintro ⟨y, rfl⟩
[GOAL]
case refine'_2.intro
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
this : CharZero ℚ
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) ↑(p ^ k)
y : CyclotomicRing (p ^ k) ℤ ℚ
⊢ IsIntegral ℤ (↑(algebraMap (CyclotomicRing (p ^ k) ℤ ℚ) (CyclotomicField (p ^ k) ℚ)) y)
[PROOFSTEP]
exact IsIntegral.algebraMap ((IsCyclotomicExtension.integral {p ^ k} ℤ _) _)
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
⊢ IsIntegralClosure (CyclotomicRing p ℤ ℚ) ℤ (CyclotomicField p ℚ)
[PROOFSTEP]
rw [← pow_one p]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
⊢ IsIntegralClosure (CyclotomicRing (p ^ 1) ℤ ℚ) ℤ (CyclotomicField (p ^ 1) ℚ)
[PROOFSTEP]
exact cyclotomicRing_isIntegralClosure_of_prime_pow
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
⊢ ↑(algebraMap { x // x ∈ 𝓞 K } K) (integralPowerBasis hζ).gen = ↑{ val := ζ, property := (_ : IsIntegral ℤ ζ) }
[PROOFSTEP]
rw [integralPowerBasis, PowerBasis.map_gen, adjoin.powerBasis'_gen]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
⊢ ↑(algebraMap { x // x ∈ 𝓞 K } K) (↑(adjoinEquivRingOfIntegers hζ) { val := ζ, property := (_ : ζ ∈ adjoin ℤ {ζ}) }) =
    ↑{ val := ζ, property := (_ : IsIntegral ℤ ζ) }
[PROOFSTEP]
simp only [adjoinEquivRingOfIntegers_apply, IsIntegralClosure.algebraMap_lift]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
⊢ ↑(algebraMap { x // x ∈ adjoin ℤ {ζ} } K) { val := ζ, property := (_ : ζ ∈ adjoin ℤ {ζ}) } = ζ
[PROOFSTEP]
rfl
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
⊢ (integralPowerBasis hζ).dim = φ ↑(p ^ k)
[PROOFSTEP]
simp [integralPowerBasis, ← cyclotomic_eq_minpoly hζ, natDegree_cyclotomic]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ IsCyclotomicExtension {p ^ 1} ℚ K
[PROOFSTEP]
convert hcycl
[GOAL]
case h.e'_1.h.e'_4
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ p ^ 1 = p
[PROOFSTEP]
rw [pow_one]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ IsPrimitiveRoot ζ ↑(p ^ 1)
[PROOFSTEP]
rwa [pow_one]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ IsCyclotomicExtension {p ^ 1} ℚ K
[PROOFSTEP]
convert hcycl
[GOAL]
case h.e'_1.h.e'_4
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ p ^ 1 = p
[PROOFSTEP]
rw [pow_one]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ IsPrimitiveRoot (?m.655556 hζ) ↑(p ^ 1)
[PROOFSTEP]
rwa [pow_one]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ IsCyclotomicExtension {p ^ 1} ℚ K
[PROOFSTEP]
convert hcycl
[GOAL]
case h.e'_1.h.e'_4
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ p ^ 1 = p
[PROOFSTEP]
rw [pow_one]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ IsPrimitiveRoot ζ ↑(p ^ 1)
[PROOFSTEP]
rwa [pow_one]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ (integralPowerBasis' hζ).dim = φ ↑p
[PROOFSTEP]
erw [@integralPowerBasis_dim p 1 K _ _ _ _ (by convert hcycl; rw [pow_one]) (by rwa [pow_one]), pow_one]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ IsCyclotomicExtension {p ^ 1} ℚ K
[PROOFSTEP]
convert hcycl
[GOAL]
case h.e'_1.h.e'_4
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ p ^ 1 = p
[PROOFSTEP]
rw [pow_one]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ IsPrimitiveRoot ζ ↑(p ^ 1)
[PROOFSTEP]
rwa [pow_one]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
inst✝¹ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
⊢ (integralPowerBasis hζ).gen ∈ adjoin ℤ {{ val := ζ - 1, property := (_ : ζ - 1 ∈ 𝓞 K) }}
[PROOFSTEP]
simp only [integralPowerBasis_gen]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
inst✝¹ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
⊢ { val := ζ, property := (_ : IsIntegral ℤ ζ) } ∈ adjoin ℤ {{ val := ζ - 1, property := (_ : ζ - 1 ∈ 𝓞 K) }}
[PROOFSTEP]
convert
  Subalgebra.add_mem _ (self_mem_adjoin_singleton ℤ (⟨ζ - 1, _⟩ : 𝓞 K))
    (Subalgebra.one_mem _)
      -- Porting note: `simp` was able to finish the proof.
[GOAL]
case h.e'_4.h.e'_3
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
inst✝¹ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
⊢ ζ = ↑({ val := ζ - 1, property := ?m.678368 } + 1)
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
inst✝¹ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
⊢ ζ - 1 ∈ 𝓞 K
[PROOFSTEP]
simp only [Subsemiring.coe_add, Subalgebra.coe_toSubsemiring, OneMemClass.coe_one, sub_add_cancel]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
inst✝¹ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
⊢ ζ - 1 ∈ 𝓞 K
[PROOFSTEP]
exact Subalgebra.sub_mem _ (hζ.isIntegral (by simp)) (Subalgebra.one_mem _)
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
inst✝¹ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
⊢ 0 < ↑(p ^ k)
[PROOFSTEP]
simp
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
inst✝¹ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
⊢ (subOneIntegralPowerBasis hζ).gen = { val := ζ - 1, property := (_ : ζ - 1 ∈ 𝓞 K) }
[PROOFSTEP]
simp [subOneIntegralPowerBasis]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ IsCyclotomicExtension {p ^ 1} ℚ K
[PROOFSTEP]
convert hcycl
[GOAL]
case h.e'_1.h.e'_4
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ p ^ 1 = p
[PROOFSTEP]
rw [pow_one]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ IsPrimitiveRoot (?m.698529 hζ) ↑(p ^ 1)
[PROOFSTEP]
rwa [pow_one]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ IsCyclotomicExtension {p ^ 1} ℚ K
[PROOFSTEP]
convert hcycl
[GOAL]
case h.e'_1.h.e'_4
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ p ^ 1 = p
[PROOFSTEP]
rw [pow_one]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ IsPrimitiveRoot ζ ↑(p ^ 1)
[PROOFSTEP]
rwa [pow_one]
