[GOAL]
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ ↑n
⊢ discr ℚ ↑(IsPrimitiveRoot.powerBasis ℚ hζ).basis = discr ℚ ↑(subOnePowerBasis ℚ hζ).basis
[PROOFSTEP]
haveI : NumberField K := @NumberField.mk _ _ _ (IsCyclotomicExtension.finiteDimensional { n } ℚ K)
[GOAL]
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ ↑n
this : NumberField K
⊢ discr ℚ ↑(IsPrimitiveRoot.powerBasis ℚ hζ).basis = discr ℚ ↑(subOnePowerBasis ℚ hζ).basis
[PROOFSTEP]
have H₁ : (aeval (hζ.powerBasis ℚ).gen) (X - 1 : ℤ[X]) = (hζ.subOnePowerBasis ℚ).gen := by simp
[GOAL]
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ ↑n
this : NumberField K
⊢ ↑(aeval (IsPrimitiveRoot.powerBasis ℚ hζ).gen) (X - 1) = (subOnePowerBasis ℚ hζ).gen
[PROOFSTEP]
simp
[GOAL]
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ ↑n
this : NumberField K
H₁ : ↑(aeval (IsPrimitiveRoot.powerBasis ℚ hζ).gen) (X - 1) = (subOnePowerBasis ℚ hζ).gen
⊢ discr ℚ ↑(IsPrimitiveRoot.powerBasis ℚ hζ).basis = discr ℚ ↑(subOnePowerBasis ℚ hζ).basis
[PROOFSTEP]
have H₂ : (aeval (hζ.subOnePowerBasis ℚ).gen) (X + 1 : ℤ[X]) = (hζ.powerBasis ℚ).gen := by simp
[GOAL]
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ ↑n
this : NumberField K
H₁ : ↑(aeval (IsPrimitiveRoot.powerBasis ℚ hζ).gen) (X - 1) = (subOnePowerBasis ℚ hζ).gen
⊢ ↑(aeval (subOnePowerBasis ℚ hζ).gen) (X + 1) = (IsPrimitiveRoot.powerBasis ℚ hζ).gen
[PROOFSTEP]
simp
[GOAL]
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ ↑n
this : NumberField K
H₁ : ↑(aeval (IsPrimitiveRoot.powerBasis ℚ hζ).gen) (X - 1) = (subOnePowerBasis ℚ hζ).gen
H₂ : ↑(aeval (subOnePowerBasis ℚ hζ).gen) (X + 1) = (IsPrimitiveRoot.powerBasis ℚ hζ).gen
⊢ discr ℚ ↑(IsPrimitiveRoot.powerBasis ℚ hζ).basis = discr ℚ ↑(subOnePowerBasis ℚ hζ).basis
[PROOFSTEP]
refine'
  discr_eq_discr_of_toMatrix_coeff_isIntegral _ (fun i j => toMatrix_isIntegral H₁ _ _ _ _) fun i j =>
    toMatrix_isIntegral H₂ _ _ _ _
[GOAL]
case refine'_1
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ ↑n
this : NumberField K
H₁ : ↑(aeval (IsPrimitiveRoot.powerBasis ℚ hζ).gen) (X - 1) = (subOnePowerBasis ℚ hζ).gen
H₂ : ↑(aeval (subOnePowerBasis ℚ hζ).gen) (X + 1) = (IsPrimitiveRoot.powerBasis ℚ hζ).gen
i : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim
j : Fin (subOnePowerBasis ℚ hζ).dim
⊢ IsIntegral ℤ (IsPrimitiveRoot.powerBasis ℚ hζ).gen
[PROOFSTEP]
exact hζ.isIntegral n.pos
[GOAL]
case refine'_2
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ ↑n
this : NumberField K
H₁ : ↑(aeval (IsPrimitiveRoot.powerBasis ℚ hζ).gen) (X - 1) = (subOnePowerBasis ℚ hζ).gen
H₂ : ↑(aeval (subOnePowerBasis ℚ hζ).gen) (X + 1) = (IsPrimitiveRoot.powerBasis ℚ hζ).gen
i : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim
j : Fin (subOnePowerBasis ℚ hζ).dim
⊢ minpoly ℚ (IsPrimitiveRoot.powerBasis ℚ hζ).gen =
    Polynomial.map (algebraMap ℤ ℚ) (minpoly ℤ (IsPrimitiveRoot.powerBasis ℚ hζ).gen)
[PROOFSTEP]
refine' minpoly.isIntegrallyClosed_eq_field_fractions' (K := ℚ) (hζ.isIntegral n.pos)
[GOAL]
case refine'_3
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ ↑n
this : NumberField K
H₁ : ↑(aeval (IsPrimitiveRoot.powerBasis ℚ hζ).gen) (X - 1) = (subOnePowerBasis ℚ hζ).gen
H₂ : ↑(aeval (subOnePowerBasis ℚ hζ).gen) (X + 1) = (IsPrimitiveRoot.powerBasis ℚ hζ).gen
i : Fin (subOnePowerBasis ℚ hζ).dim
j : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim
⊢ IsIntegral ℤ (subOnePowerBasis ℚ hζ).gen
[PROOFSTEP]
exact isIntegral_sub (hζ.isIntegral n.pos) isIntegral_one
[GOAL]
case refine'_4
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ ↑n
this : NumberField K
H₁ : ↑(aeval (IsPrimitiveRoot.powerBasis ℚ hζ).gen) (X - 1) = (subOnePowerBasis ℚ hζ).gen
H₂ : ↑(aeval (subOnePowerBasis ℚ hζ).gen) (X + 1) = (IsPrimitiveRoot.powerBasis ℚ hζ).gen
i : Fin (subOnePowerBasis ℚ hζ).dim
j : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim
⊢ minpoly ℚ (subOnePowerBasis ℚ hζ).gen = Polynomial.map (algebraMap ℤ ℚ) (minpoly ℤ (subOnePowerBasis ℚ hζ).gen)
[PROOFSTEP]
refine' minpoly.isIntegrallyClosed_eq_field_fractions' (K := ℚ) _
[GOAL]
case refine'_4
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ ↑n
this : NumberField K
H₁ : ↑(aeval (IsPrimitiveRoot.powerBasis ℚ hζ).gen) (X - 1) = (subOnePowerBasis ℚ hζ).gen
H₂ : ↑(aeval (subOnePowerBasis ℚ hζ).gen) (X + 1) = (IsPrimitiveRoot.powerBasis ℚ hζ).gen
i : Fin (subOnePowerBasis ℚ hζ).dim
j : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim
⊢ IsIntegral ℤ (subOnePowerBasis ℚ hζ).gen
[PROOFSTEP]
exact isIntegral_sub (hζ.isIntegral n.pos) isIntegral_one
[GOAL]
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hk : p ^ (k + 1) ≠ 2
⊢ discr K ↑(IsPrimitiveRoot.powerBasis K hζ).basis =
    ↑((-1) ^ (φ ↑(p ^ (k + 1)) / 2)) * ↑↑(p ^ (↑p ^ k * ((↑p - 1) * (k + 1) - 1)))
[PROOFSTEP]
haveI hne := IsCyclotomicExtension.neZero' (p ^ (k + 1)) K L
[GOAL]
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑↑(p ^ (k + 1))
⊢ discr K ↑(IsPrimitiveRoot.powerBasis K hζ).basis =
    ↑((-1) ^ (φ ↑(p ^ (k + 1)) / 2)) * ↑↑(p ^ (↑p ^ k * ((↑p - 1) * (k + 1) - 1)))
[PROOFSTEP]
haveI mf : Module.Finite K L := finiteDimensional {p ^ (k + 1)} K L
[GOAL]
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑↑(p ^ (k + 1))
mf : Module.Finite K L
⊢ discr K ↑(IsPrimitiveRoot.powerBasis K hζ).basis =
    ↑((-1) ^ (φ ↑(p ^ (k + 1)) / 2)) * ↑↑(p ^ (↑p ^ k * ((↑p - 1) * (k + 1) - 1)))
[PROOFSTEP]
haveI se : IsSeparable K L := (isGalois (p ^ (k + 1)) K L).to_isSeparable
[GOAL]
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑↑(p ^ (k + 1))
mf : Module.Finite K L
se : IsSeparable K L
⊢ discr K ↑(IsPrimitiveRoot.powerBasis K hζ).basis =
    ↑((-1) ^ (φ ↑(p ^ (k + 1)) / 2)) * ↑↑(p ^ (↑p ^ k * ((↑p - 1) * (k + 1) - 1)))
[PROOFSTEP]
rw [discr_powerBasis_eq_norm, finrank L hirr, hζ.powerBasis_gen _, ← hζ.minpoly_eq_cyclotomic_of_irreducible hirr,
  PNat.pow_coe, totient_prime_pow hp.out (succ_pos k), succ_sub_one]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑↑(p ^ (k + 1))
mf : Module.Finite K L
se : IsSeparable K L
⊢ (-1) ^ (↑p ^ k * (↑p - 1) * (↑p ^ k * (↑p - 1) - 1) / 2) *
      ↑(Algebra.norm K) (↑(aeval ζ) (↑derivative (cyclotomic (↑p ^ (k + 1)) K))) =
    ↑((-1) ^ (↑p ^ k * (↑p - 1) / 2)) * ↑↑(p ^ (↑p ^ k * ((↑p - 1) * (k + 1) - 1)))
[PROOFSTEP]
have coe_two : ((2 : ℕ+) : ℕ) = 2 := rfl
[GOAL]
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑↑(p ^ (k + 1))
mf : Module.Finite K L
se : IsSeparable K L
coe_two : ↑2 = 2
⊢ (-1) ^ (↑p ^ k * (↑p - 1) * (↑p ^ k * (↑p - 1) - 1) / 2) *
      ↑(Algebra.norm K) (↑(aeval ζ) (↑derivative (cyclotomic (↑p ^ (k + 1)) K))) =
    ↑((-1) ^ (↑p ^ k * (↑p - 1) / 2)) * ↑↑(p ^ (↑p ^ k * ((↑p - 1) * (k + 1) - 1)))
[PROOFSTEP]
have hp2 : p = 2 → k ≠ 0 := by
  rintro rfl rfl
  exact absurd rfl hk
[GOAL]
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑↑(p ^ (k + 1))
mf : Module.Finite K L
se : IsSeparable K L
coe_two : ↑2 = 2
⊢ p = 2 → k ≠ 0
[PROOFSTEP]
rintro rfl rfl
[GOAL]
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
mf : Module.Finite K L
se : IsSeparable K L
coe_two : ↑2 = 2
hp : Fact (Nat.Prime ↑2)
inst✝ : IsCyclotomicExtension {2 ^ (0 + 1)} K L
hζ : IsPrimitiveRoot ζ ↑(2 ^ (0 + 1))
hirr : Irreducible (cyclotomic (↑(2 ^ (0 + 1))) K)
hk : 2 ^ (0 + 1) ≠ 2
hne : NeZero ↑↑(2 ^ (0 + 1))
⊢ False
[PROOFSTEP]
exact absurd rfl hk
[GOAL]
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑↑(p ^ (k + 1))
mf : Module.Finite K L
se : IsSeparable K L
coe_two : ↑2 = 2
hp2 : p = 2 → k ≠ 0
⊢ (-1) ^ (↑p ^ k * (↑p - 1) * (↑p ^ k * (↑p - 1) - 1) / 2) *
      ↑(Algebra.norm K) (↑(aeval ζ) (↑derivative (cyclotomic (↑p ^ (k + 1)) K))) =
    ↑((-1) ^ (↑p ^ k * (↑p - 1) / 2)) * ↑↑(p ^ (↑p ^ k * ((↑p - 1) * (k + 1) - 1)))
[PROOFSTEP]
congr 1
[GOAL]
case e_a
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑↑(p ^ (k + 1))
mf : Module.Finite K L
se : IsSeparable K L
coe_two : ↑2 = 2
hp2 : p = 2 → k ≠ 0
⊢ (-1) ^ (↑p ^ k * (↑p - 1) * (↑p ^ k * (↑p - 1) - 1) / 2) = ↑((-1) ^ (↑p ^ k * (↑p - 1) / 2))
[PROOFSTEP]
rcases eq_or_ne p 2 with (rfl | hp2)
[GOAL]
case e_a.inl
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
mf : Module.Finite K L
se : IsSeparable K L
coe_two : ↑2 = 2
inst✝ : IsCyclotomicExtension {2 ^ (k + 1)} K L
hp : Fact (Nat.Prime ↑2)
hζ : IsPrimitiveRoot ζ ↑(2 ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(2 ^ (k + 1))) K)
hk : 2 ^ (k + 1) ≠ 2
hne : NeZero ↑↑(2 ^ (k + 1))
hp2 : 2 = 2 → k ≠ 0
⊢ (-1) ^ (↑2 ^ k * (↑2 - 1) * (↑2 ^ k * (↑2 - 1) - 1) / 2) = ↑((-1) ^ (↑2 ^ k * (↑2 - 1) / 2))
[PROOFSTEP]
rcases Nat.exists_eq_succ_of_ne_zero (hp2 rfl) with ⟨k, rfl⟩
[GOAL]
case e_a.inl.intro
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
mf : Module.Finite K L
se : IsSeparable K L
coe_two : ↑2 = 2
hp : Fact (Nat.Prime ↑2)
k : ℕ
inst✝ : IsCyclotomicExtension {2 ^ (succ k + 1)} K L
hζ : IsPrimitiveRoot ζ ↑(2 ^ (succ k + 1))
hirr : Irreducible (cyclotomic (↑(2 ^ (succ k + 1))) K)
hk : 2 ^ (succ k + 1) ≠ 2
hne : NeZero ↑↑(2 ^ (succ k + 1))
hp2 : 2 = 2 → succ k ≠ 0
⊢ (-1) ^ (↑2 ^ succ k * (↑2 - 1) * (↑2 ^ succ k * (↑2 - 1) - 1) / 2) = ↑((-1) ^ (↑2 ^ succ k * (↑2 - 1) / 2))
[PROOFSTEP]
rw [coe_two, succ_sub_succ_eq_sub, tsub_zero, mul_one]
[GOAL]
case e_a.inl.intro
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
mf : Module.Finite K L
se : IsSeparable K L
coe_two : ↑2 = 2
hp : Fact (Nat.Prime ↑2)
k : ℕ
inst✝ : IsCyclotomicExtension {2 ^ (succ k + 1)} K L
hζ : IsPrimitiveRoot ζ ↑(2 ^ (succ k + 1))
hirr : Irreducible (cyclotomic (↑(2 ^ (succ k + 1))) K)
hk : 2 ^ (succ k + 1) ≠ 2
hne : NeZero ↑↑(2 ^ (succ k + 1))
hp2 : 2 = 2 → succ k ≠ 0
⊢ (-1) ^ (2 ^ succ k * (2 ^ succ k - 1) / 2) = ↑((-1) ^ (2 ^ succ k / 2))
[PROOFSTEP]
simp only [_root_.pow_succ]
[GOAL]
case e_a.inl.intro
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
mf : Module.Finite K L
se : IsSeparable K L
coe_two : ↑2 = 2
hp : Fact (Nat.Prime ↑2)
k : ℕ
inst✝ : IsCyclotomicExtension {2 ^ (succ k + 1)} K L
hζ : IsPrimitiveRoot ζ ↑(2 ^ (succ k + 1))
hirr : Irreducible (cyclotomic (↑(2 ^ (succ k + 1))) K)
hk : 2 ^ (succ k + 1) ≠ 2
hne : NeZero ↑↑(2 ^ (succ k + 1))
hp2 : 2 = 2 → succ k ≠ 0
⊢ (-1) ^ (2 * 2 ^ k * (2 * 2 ^ k - 1) / 2) = ↑((-1) ^ (2 * 2 ^ k / 2))
[PROOFSTEP]
rw [mul_assoc, Nat.mul_div_cancel_left _ zero_lt_two, Nat.mul_div_cancel_left _ zero_lt_two]
[GOAL]
case e_a.inl.intro
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
mf : Module.Finite K L
se : IsSeparable K L
coe_two : ↑2 = 2
hp : Fact (Nat.Prime ↑2)
k : ℕ
inst✝ : IsCyclotomicExtension {2 ^ (succ k + 1)} K L
hζ : IsPrimitiveRoot ζ ↑(2 ^ (succ k + 1))
hirr : Irreducible (cyclotomic (↑(2 ^ (succ k + 1))) K)
hk : 2 ^ (succ k + 1) ≠ 2
hne : NeZero ↑↑(2 ^ (succ k + 1))
hp2 : 2 = 2 → succ k ≠ 0
⊢ (-1) ^ (2 ^ k * (2 * 2 ^ k - 1)) = ↑((-1) ^ 2 ^ k)
[PROOFSTEP]
cases k
[GOAL]
case e_a.inl.intro.zero
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
mf : Module.Finite K L
se : IsSeparable K L
coe_two : ↑2 = 2
hp : Fact (Nat.Prime ↑2)
inst✝ : IsCyclotomicExtension {2 ^ (succ Nat.zero + 1)} K L
hζ : IsPrimitiveRoot ζ ↑(2 ^ (succ Nat.zero + 1))
hirr : Irreducible (cyclotomic (↑(2 ^ (succ Nat.zero + 1))) K)
hk : 2 ^ (succ Nat.zero + 1) ≠ 2
hne : NeZero ↑↑(2 ^ (succ Nat.zero + 1))
hp2 : 2 = 2 → succ Nat.zero ≠ 0
⊢ (-1) ^ (2 ^ Nat.zero * (2 * 2 ^ Nat.zero - 1)) = ↑((-1) ^ 2 ^ Nat.zero)
[PROOFSTEP]
simp
[GOAL]
case e_a.inl.intro.succ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
mf : Module.Finite K L
se : IsSeparable K L
coe_two : ↑2 = 2
hp : Fact (Nat.Prime ↑2)
n✝ : ℕ
inst✝ : IsCyclotomicExtension {2 ^ (succ (succ n✝) + 1)} K L
hζ : IsPrimitiveRoot ζ ↑(2 ^ (succ (succ n✝) + 1))
hirr : Irreducible (cyclotomic (↑(2 ^ (succ (succ n✝) + 1))) K)
hk : 2 ^ (succ (succ n✝) + 1) ≠ 2
hne : NeZero ↑↑(2 ^ (succ (succ n✝) + 1))
hp2 : 2 = 2 → succ (succ n✝) ≠ 0
⊢ (-1) ^ (2 ^ succ n✝ * (2 * 2 ^ succ n✝ - 1)) = ↑((-1) ^ 2 ^ succ n✝)
[PROOFSTEP]
norm_num
[GOAL]
case e_a.inl.intro.succ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
mf : Module.Finite K L
se : IsSeparable K L
coe_two : ↑2 = 2
hp : Fact (Nat.Prime ↑2)
n✝ : ℕ
inst✝ : IsCyclotomicExtension {2 ^ (succ (succ n✝) + 1)} K L
hζ : IsPrimitiveRoot ζ ↑(2 ^ (succ (succ n✝) + 1))
hirr : Irreducible (cyclotomic (↑(2 ^ (succ (succ n✝) + 1))) K)
hk : 2 ^ (succ (succ n✝) + 1) ≠ 2
hne : NeZero ↑↑(2 ^ (succ (succ n✝) + 1))
hp2 : 2 = 2 → succ (succ n✝) ≠ 0
⊢ (-1) ^ (2 ^ succ n✝ * (2 * 2 ^ succ n✝ - 1)) = (-1) ^ 2 ^ succ n✝
[PROOFSTEP]
simp_rw [_root_.pow_succ, (even_two.mul_right _).neg_one_pow, ((even_two.mul_right _).mul_right _).neg_one_pow]
[GOAL]
case e_a.inr
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑↑(p ^ (k + 1))
mf : Module.Finite K L
se : IsSeparable K L
coe_two : ↑2 = 2
hp2✝ : p = 2 → k ≠ 0
hp2 : p ≠ 2
⊢ (-1) ^ (↑p ^ k * (↑p - 1) * (↑p ^ k * (↑p - 1) - 1) / 2) = ↑((-1) ^ (↑p ^ k * (↑p - 1) / 2))
[PROOFSTEP]
replace hp2 : (p : ℕ) ≠ 2
[GOAL]
case hp2
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑↑(p ^ (k + 1))
mf : Module.Finite K L
se : IsSeparable K L
coe_two : ↑2 = 2
hp2✝ : p = 2 → k ≠ 0
hp2 : p ≠ 2
⊢ ↑p ≠ 2
[PROOFSTEP]
rwa [Ne.def, ← coe_two, PNat.coe_inj]
[GOAL]
case e_a.inr
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑↑(p ^ (k + 1))
mf : Module.Finite K L
se : IsSeparable K L
coe_two : ↑2 = 2
hp2✝ : p = 2 → k ≠ 0
hp2 : ↑p ≠ 2
⊢ (-1) ^ (↑p ^ k * (↑p - 1) * (↑p ^ k * (↑p - 1) - 1) / 2) = ↑((-1) ^ (↑p ^ k * (↑p - 1) / 2))
[PROOFSTEP]
have hpo : Odd (p : ℕ) := hp.out.odd_of_ne_two hp2
[GOAL]
case e_a.inr
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑↑(p ^ (k + 1))
mf : Module.Finite K L
se : IsSeparable K L
coe_two : ↑2 = 2
hp2✝ : p = 2 → k ≠ 0
hp2 : ↑p ≠ 2
hpo : Odd ↑p
⊢ (-1) ^ (↑p ^ k * (↑p - 1) * (↑p ^ k * (↑p - 1) - 1) / 2) = ↑((-1) ^ (↑p ^ k * (↑p - 1) / 2))
[PROOFSTEP]
obtain ⟨a, ha⟩ := (hp.out.even_sub_one hp2).two_dvd
[GOAL]
case e_a.inr.intro
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑↑(p ^ (k + 1))
mf : Module.Finite K L
se : IsSeparable K L
coe_two : ↑2 = 2
hp2✝ : p = 2 → k ≠ 0
hp2 : ↑p ≠ 2
hpo : Odd ↑p
a : ℕ
ha : ↑p - 1 = 2 * a
⊢ (-1) ^ (↑p ^ k * (↑p - 1) * (↑p ^ k * (↑p - 1) - 1) / 2) = ↑((-1) ^ (↑p ^ k * (↑p - 1) / 2))
[PROOFSTEP]
rw [ha, mul_left_comm, mul_assoc, Nat.mul_div_cancel_left _ two_pos, Nat.mul_div_cancel_left _ two_pos, mul_right_comm,
  pow_mul, (hpo.pow.mul _).neg_one_pow, pow_mul, hpo.pow.neg_one_pow]
[GOAL]
case e_a.inr.intro
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑↑(p ^ (k + 1))
mf : Module.Finite K L
se : IsSeparable K L
coe_two : ↑2 = 2
hp2✝ : p = 2 → k ≠ 0
hp2 : ↑p ≠ 2
hpo : Odd ↑p
a : ℕ
ha : ↑p - 1 = 2 * a
⊢ (-1) ^ a = ↑((-1) ^ a)
[PROOFSTEP]
norm_cast
[GOAL]
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑↑(p ^ (k + 1))
mf : Module.Finite K L
se : IsSeparable K L
coe_two : ↑2 = 2
hp2✝ : p = 2 → k ≠ 0
hp2 : ↑p ≠ 2
hpo : Odd ↑p
a : ℕ
ha : ↑p - 1 = 2 * a
⊢ Odd (2 * (↑p ^ k * a) - 1)
[PROOFSTEP]
refine' Nat.Even.sub_odd _ (even_two_mul _) odd_one
[GOAL]
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑↑(p ^ (k + 1))
mf : Module.Finite K L
se : IsSeparable K L
coe_two : ↑2 = 2
hp2✝ : p = 2 → k ≠ 0
hp2 : ↑p ≠ 2
hpo : Odd ↑p
a : ℕ
ha : ↑p - 1 = 2 * a
⊢ 1 ≤ 2 * (↑p ^ k * a)
[PROOFSTEP]
rw [mul_left_comm, ← ha]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑↑(p ^ (k + 1))
mf : Module.Finite K L
se : IsSeparable K L
coe_two : ↑2 = 2
hp2✝ : p = 2 → k ≠ 0
hp2 : ↑p ≠ 2
hpo : Odd ↑p
a : ℕ
ha : ↑p - 1 = 2 * a
⊢ 1 ≤ ↑p ^ k * (↑p - 1)
[PROOFSTEP]
exact one_le_mul (one_le_pow _ _ hp.1.pos) (succ_le_iff.2 <| tsub_pos_of_lt hp.1.one_lt)
[GOAL]
case e_a
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑↑(p ^ (k + 1))
mf : Module.Finite K L
se : IsSeparable K L
coe_two : ↑2 = 2
hp2 : p = 2 → k ≠ 0
⊢ ↑(Algebra.norm K) (↑(aeval ζ) (↑derivative (cyclotomic (↑p ^ (k + 1)) K))) =
    ↑↑(p ^ (↑p ^ k * ((↑p - 1) * (k + 1) - 1)))
[PROOFSTEP]
have H := congr_arg (@derivative K _) (cyclotomic_prime_pow_mul_X_pow_sub_one K p k)
[GOAL]
case e_a
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑↑(p ^ (k + 1))
mf : Module.Finite K L
se : IsSeparable K L
coe_two : ↑2 = 2
hp2 : p = 2 → k ≠ 0
H : ↑derivative (cyclotomic (↑p ^ (k + 1)) K * (X ^ ↑p ^ k - 1)) = ↑derivative (X ^ ↑p ^ (k + 1) - 1)
⊢ ↑(Algebra.norm K) (↑(aeval ζ) (↑derivative (cyclotomic (↑p ^ (k + 1)) K))) =
    ↑↑(p ^ (↑p ^ k * ((↑p - 1) * (k + 1) - 1)))
[PROOFSTEP]
rw [derivative_mul, derivative_sub, derivative_one, sub_zero, derivative_X_pow, C_eq_nat_cast, derivative_sub,
  derivative_one, sub_zero, derivative_X_pow, C_eq_nat_cast, ← PNat.pow_coe,
  hζ.minpoly_eq_cyclotomic_of_irreducible hirr] at H
[GOAL]
case e_a
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑↑(p ^ (k + 1))
mf : Module.Finite K L
se : IsSeparable K L
coe_two : ↑2 = 2
hp2 : p = 2 → k ≠ 0
H :
  ↑derivative (minpoly K ζ) * (X ^ ↑p ^ k - 1) + minpoly K ζ * (↑(↑p ^ k) * X ^ (↑p ^ k - 1)) =
    ↑↑(p ^ (k + 1)) * X ^ (↑(p ^ (k + 1)) - 1)
⊢ ↑(Algebra.norm K) (↑(aeval ζ) (↑derivative (cyclotomic (↑p ^ (k + 1)) K))) =
    ↑↑(p ^ (↑p ^ k * ((↑p - 1) * (k + 1) - 1)))
[PROOFSTEP]
replace H := congr_arg (fun P => aeval ζ P) H
[GOAL]
case e_a
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑↑(p ^ (k + 1))
mf : Module.Finite K L
se : IsSeparable K L
coe_two : ↑2 = 2
hp2 : p = 2 → k ≠ 0
H :
  (fun P => ↑(aeval ζ) P)
      (↑derivative (minpoly K ζ) * (X ^ ↑p ^ k - 1) + minpoly K ζ * (↑(↑p ^ k) * X ^ (↑p ^ k - 1))) =
    (fun P => ↑(aeval ζ) P) (↑↑(p ^ (k + 1)) * X ^ (↑(p ^ (k + 1)) - 1))
⊢ ↑(Algebra.norm K) (↑(aeval ζ) (↑derivative (cyclotomic (↑p ^ (k + 1)) K))) =
    ↑↑(p ^ (↑p ^ k * ((↑p - 1) * (k + 1) - 1)))
[PROOFSTEP]
simp only [aeval_add, aeval_mul, minpoly.aeval, zero_mul, add_zero, aeval_nat_cast, _root_.map_sub, aeval_one,
  aeval_X_pow] at H
[GOAL]
case e_a
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑↑(p ^ (k + 1))
mf : Module.Finite K L
se : IsSeparable K L
coe_two : ↑2 = 2
hp2 : p = 2 → k ≠ 0
H : ↑(aeval ζ) (↑derivative (minpoly K ζ)) * (ζ ^ ↑p ^ k - 1) = ↑↑(p ^ (k + 1)) * ζ ^ (↑(p ^ (k + 1)) - 1)
⊢ ↑(Algebra.norm K) (↑(aeval ζ) (↑derivative (cyclotomic (↑p ^ (k + 1)) K))) =
    ↑↑(p ^ (↑p ^ k * ((↑p - 1) * (k + 1) - 1)))
[PROOFSTEP]
replace H := congr_arg (Algebra.norm K) H
[GOAL]
case e_a
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑↑(p ^ (k + 1))
mf : Module.Finite K L
se : IsSeparable K L
coe_two : ↑2 = 2
hp2 : p = 2 → k ≠ 0
H :
  ↑(Algebra.norm K) (↑(aeval ζ) (↑derivative (minpoly K ζ)) * (ζ ^ ↑p ^ k - 1)) =
    ↑(Algebra.norm K) (↑↑(p ^ (k + 1)) * ζ ^ (↑(p ^ (k + 1)) - 1))
⊢ ↑(Algebra.norm K) (↑(aeval ζ) (↑derivative (cyclotomic (↑p ^ (k + 1)) K))) =
    ↑↑(p ^ (↑p ^ k * ((↑p - 1) * (k + 1) - 1)))
[PROOFSTEP]
have hnorm : (norm K) (ζ ^ (p : ℕ) ^ k - 1) = (p : K) ^ (p : ℕ) ^ k :=
  by
  by_cases hp : p = 2
  · exact_mod_cast hζ.pow_sub_one_norm_prime_pow_of_ne_zero hirr le_rfl (hp2 hp)
  · exact_mod_cast hζ.pow_sub_one_norm_prime_ne_two hirr le_rfl hp
[GOAL]
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑↑(p ^ (k + 1))
mf : Module.Finite K L
se : IsSeparable K L
coe_two : ↑2 = 2
hp2 : p = 2 → k ≠ 0
H :
  ↑(Algebra.norm K) (↑(aeval ζ) (↑derivative (minpoly K ζ)) * (ζ ^ ↑p ^ k - 1)) =
    ↑(Algebra.norm K) (↑↑(p ^ (k + 1)) * ζ ^ (↑(p ^ (k + 1)) - 1))
⊢ ↑(Algebra.norm K) (ζ ^ ↑p ^ k - 1) = ↑↑p ^ ↑p ^ k
[PROOFSTEP]
by_cases hp : p = 2
[GOAL]
case pos
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp✝ : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑↑(p ^ (k + 1))
mf : Module.Finite K L
se : IsSeparable K L
coe_two : ↑2 = 2
hp2 : p = 2 → k ≠ 0
H :
  ↑(Algebra.norm K) (↑(aeval ζ) (↑derivative (minpoly K ζ)) * (ζ ^ ↑p ^ k - 1)) =
    ↑(Algebra.norm K) (↑↑(p ^ (k + 1)) * ζ ^ (↑(p ^ (k + 1)) - 1))
hp : p = 2
⊢ ↑(Algebra.norm K) (ζ ^ ↑p ^ k - 1) = ↑↑p ^ ↑p ^ k
[PROOFSTEP]
exact_mod_cast hζ.pow_sub_one_norm_prime_pow_of_ne_zero hirr le_rfl (hp2 hp)
[GOAL]
case neg
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp✝ : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑↑(p ^ (k + 1))
mf : Module.Finite K L
se : IsSeparable K L
coe_two : ↑2 = 2
hp2 : p = 2 → k ≠ 0
H :
  ↑(Algebra.norm K) (↑(aeval ζ) (↑derivative (minpoly K ζ)) * (ζ ^ ↑p ^ k - 1)) =
    ↑(Algebra.norm K) (↑↑(p ^ (k + 1)) * ζ ^ (↑(p ^ (k + 1)) - 1))
hp : ¬p = 2
⊢ ↑(Algebra.norm K) (ζ ^ ↑p ^ k - 1) = ↑↑p ^ ↑p ^ k
[PROOFSTEP]
exact_mod_cast hζ.pow_sub_one_norm_prime_ne_two hirr le_rfl hp
[GOAL]
case e_a
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑↑(p ^ (k + 1))
mf : Module.Finite K L
se : IsSeparable K L
coe_two : ↑2 = 2
hp2 : p = 2 → k ≠ 0
H :
  ↑(Algebra.norm K) (↑(aeval ζ) (↑derivative (minpoly K ζ)) * (ζ ^ ↑p ^ k - 1)) =
    ↑(Algebra.norm K) (↑↑(p ^ (k + 1)) * ζ ^ (↑(p ^ (k + 1)) - 1))
hnorm : ↑(Algebra.norm K) (ζ ^ ↑p ^ k - 1) = ↑↑p ^ ↑p ^ k
⊢ ↑(Algebra.norm K) (↑(aeval ζ) (↑derivative (cyclotomic (↑p ^ (k + 1)) K))) =
    ↑↑(p ^ (↑p ^ k * ((↑p - 1) * (k + 1) - 1)))
[PROOFSTEP]
rw [MonoidHom.map_mul, hnorm, MonoidHom.map_mul, ← map_natCast (algebraMap K L), Algebra.norm_algebraMap,
  finrank L hirr] at H
[GOAL]
case e_a
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑↑(p ^ (k + 1))
mf : Module.Finite K L
se : IsSeparable K L
coe_two : ↑2 = 2
hp2 : p = 2 → k ≠ 0
H :
  ↑(Algebra.norm K) (↑(aeval ζ) (↑derivative (minpoly K ζ))) * ↑↑p ^ ↑p ^ k =
    ↑↑(p ^ (k + 1)) ^ φ ↑(p ^ (k + 1)) * ↑(Algebra.norm K) (ζ ^ (↑(p ^ (k + 1)) - 1))
hnorm : ↑(Algebra.norm K) (ζ ^ ↑p ^ k - 1) = ↑↑p ^ ↑p ^ k
⊢ ↑(Algebra.norm K) (↑(aeval ζ) (↑derivative (cyclotomic (↑p ^ (k + 1)) K))) =
    ↑↑(p ^ (↑p ^ k * ((↑p - 1) * (k + 1) - 1)))
[PROOFSTEP]
conv_rhs at H =>
  -- Porting note: need to drill down to successfully rewrite the totient
  enter [1, 2]
  rw [PNat.pow_coe, ← succ_eq_add_one, totient_prime_pow hp.out (succ_pos k), Nat.sub_one, Nat.pred_succ]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑↑(p ^ (k + 1))
mf : Module.Finite K L
se : IsSeparable K L
coe_two : ↑2 = 2
hp2 : p = 2 → k ≠ 0
H :
  ↑(Algebra.norm K) (↑(aeval ζ) (↑derivative (minpoly K ζ))) * ↑↑p ^ ↑p ^ k =
    ↑↑(p ^ (k + 1)) ^ φ ↑(p ^ (k + 1)) * ↑(Algebra.norm K) (ζ ^ (↑(p ^ (k + 1)) - 1))
hnorm : ↑(Algebra.norm K) (ζ ^ ↑p ^ k - 1) = ↑↑p ^ ↑p ^ k
| ↑↑(p ^ (k + 1)) ^ φ ↑(p ^ (k + 1)) * ↑(Algebra.norm K) (ζ ^ (↑(p ^ (k + 1)) - 1))
[PROOFSTEP]
  enter [1, 2]
  rw [PNat.pow_coe, ← succ_eq_add_one, totient_prime_pow hp.out (succ_pos k), Nat.sub_one, Nat.pred_succ]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑↑(p ^ (k + 1))
mf : Module.Finite K L
se : IsSeparable K L
coe_two : ↑2 = 2
hp2 : p = 2 → k ≠ 0
H :
  ↑(Algebra.norm K) (↑(aeval ζ) (↑derivative (minpoly K ζ))) * ↑↑p ^ ↑p ^ k =
    ↑↑(p ^ (k + 1)) ^ φ ↑(p ^ (k + 1)) * ↑(Algebra.norm K) (ζ ^ (↑(p ^ (k + 1)) - 1))
hnorm : ↑(Algebra.norm K) (ζ ^ ↑p ^ k - 1) = ↑↑p ^ ↑p ^ k
| ↑↑(p ^ (k + 1)) ^ φ ↑(p ^ (k + 1)) * ↑(Algebra.norm K) (ζ ^ (↑(p ^ (k + 1)) - 1))
[PROOFSTEP]
  enter [1, 2]
  rw [PNat.pow_coe, ← succ_eq_add_one, totient_prime_pow hp.out (succ_pos k), Nat.sub_one, Nat.pred_succ]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑↑(p ^ (k + 1))
mf : Module.Finite K L
se : IsSeparable K L
coe_two : ↑2 = 2
hp2 : p = 2 → k ≠ 0
H :
  ↑(Algebra.norm K) (↑(aeval ζ) (↑derivative (minpoly K ζ))) * ↑↑p ^ ↑p ^ k =
    ↑↑(p ^ (k + 1)) ^ φ ↑(p ^ (k + 1)) * ↑(Algebra.norm K) (ζ ^ (↑(p ^ (k + 1)) - 1))
hnorm : ↑(Algebra.norm K) (ζ ^ ↑p ^ k - 1) = ↑↑p ^ ↑p ^ k
| ↑↑(p ^ (k + 1)) ^ φ ↑(p ^ (k + 1)) * ↑(Algebra.norm K) (ζ ^ (↑(p ^ (k + 1)) - 1))
[PROOFSTEP]
enter [1, 2]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑↑(p ^ (k + 1))
mf : Module.Finite K L
se : IsSeparable K L
coe_two : ↑2 = 2
hp2 : p = 2 → k ≠ 0
H :
  ↑(Algebra.norm K) (↑(aeval ζ) (↑derivative (minpoly K ζ))) * ↑↑p ^ ↑p ^ k =
    ↑↑(p ^ (k + 1)) ^ φ ↑(p ^ (k + 1)) * ↑(Algebra.norm K) (ζ ^ (↑(p ^ (k + 1)) - 1))
hnorm : ↑(Algebra.norm K) (ζ ^ ↑p ^ k - 1) = ↑↑p ^ ↑p ^ k
| φ ↑(p ^ (k + 1))
[PROOFSTEP]
rw [PNat.pow_coe, ← succ_eq_add_one, totient_prime_pow hp.out (succ_pos k), Nat.sub_one, Nat.pred_succ]
[GOAL]
case e_a
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑↑(p ^ (k + 1))
mf : Module.Finite K L
se : IsSeparable K L
coe_two : ↑2 = 2
hp2 : p = 2 → k ≠ 0
H :
  ↑(Algebra.norm K) (↑(aeval ζ) (↑derivative (minpoly K ζ))) * ↑↑p ^ ↑p ^ k =
    ↑↑(p ^ (k + 1)) ^ (↑p ^ k * (↑p - 1)) * ↑(Algebra.norm K) (ζ ^ (↑(p ^ (k + 1)) - 1))
hnorm : ↑(Algebra.norm K) (ζ ^ ↑p ^ k - 1) = ↑↑p ^ ↑p ^ k
⊢ ↑(Algebra.norm K) (↑(aeval ζ) (↑derivative (cyclotomic (↑p ^ (k + 1)) K))) =
    ↑↑(p ^ (↑p ^ k * ((↑p - 1) * (k + 1) - 1)))
[PROOFSTEP]
rw [← hζ.minpoly_eq_cyclotomic_of_irreducible hirr, map_pow, hζ.norm_eq_one hk hirr, one_pow, mul_one, PNat.pow_coe,
  cast_pow, ← pow_mul, ← mul_assoc, mul_comm (k + 1), mul_assoc] at H
[GOAL]
case e_a
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑↑(p ^ (k + 1))
mf : Module.Finite K L
se : IsSeparable K L
coe_two : ↑2 = 2
hp2 : p = 2 → k ≠ 0
H :
  ↑(Algebra.norm K) (↑(aeval ζ) (↑derivative (cyclotomic (↑p ^ (k + 1)) K))) * ↑↑p ^ ↑p ^ k =
    ↑↑p ^ (↑p ^ k * ((k + 1) * (↑p - 1)))
hnorm : ↑(Algebra.norm K) (ζ ^ ↑p ^ k - 1) = ↑↑p ^ ↑p ^ k
⊢ ↑(Algebra.norm K) (↑(aeval ζ) (↑derivative (cyclotomic (↑p ^ (k + 1)) K))) =
    ↑↑(p ^ (↑p ^ k * ((↑p - 1) * (k + 1) - 1)))
[PROOFSTEP]
have := mul_pos (succ_pos k) (tsub_pos_of_lt hp.out.one_lt)
[GOAL]
case e_a
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑↑(p ^ (k + 1))
mf : Module.Finite K L
se : IsSeparable K L
coe_two : ↑2 = 2
hp2 : p = 2 → k ≠ 0
H :
  ↑(Algebra.norm K) (↑(aeval ζ) (↑derivative (cyclotomic (↑p ^ (k + 1)) K))) * ↑↑p ^ ↑p ^ k =
    ↑↑p ^ (↑p ^ k * ((k + 1) * (↑p - 1)))
hnorm : ↑(Algebra.norm K) (ζ ^ ↑p ^ k - 1) = ↑↑p ^ ↑p ^ k
this : 0 < succ k * (↑p - 1)
⊢ ↑(Algebra.norm K) (↑(aeval ζ) (↑derivative (cyclotomic (↑p ^ (k + 1)) K))) =
    ↑↑(p ^ (↑p ^ k * ((↑p - 1) * (k + 1) - 1)))
[PROOFSTEP]
rw [← succ_pred_eq_of_pos this, mul_succ, pow_add _ _ ((p : ℕ) ^ k)] at H
[GOAL]
case e_a
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑↑(p ^ (k + 1))
mf : Module.Finite K L
se : IsSeparable K L
coe_two : ↑2 = 2
hp2 : p = 2 → k ≠ 0
H :
  ↑(Algebra.norm K) (↑(aeval ζ) (↑derivative (cyclotomic (↑p ^ (k + 1)) K))) * ↑↑p ^ ↑p ^ k =
    ↑↑p ^ (↑p ^ k * pred (succ k * (↑p - 1))) * ↑↑p ^ ↑p ^ k
hnorm : ↑(Algebra.norm K) (ζ ^ ↑p ^ k - 1) = ↑↑p ^ ↑p ^ k
this : 0 < succ k * (↑p - 1)
⊢ ↑(Algebra.norm K) (↑(aeval ζ) (↑derivative (cyclotomic (↑p ^ (k + 1)) K))) =
    ↑↑(p ^ (↑p ^ k * ((↑p - 1) * (k + 1) - 1)))
[PROOFSTEP]
replace H := (mul_left_inj' fun h => ?_).1 H
[GOAL]
case e_a.refine_2
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑↑(p ^ (k + 1))
mf : Module.Finite K L
se : IsSeparable K L
coe_two : ↑2 = 2
hp2 : p = 2 → k ≠ 0
hnorm : ↑(Algebra.norm K) (ζ ^ ↑p ^ k - 1) = ↑↑p ^ ↑p ^ k
this : 0 < succ k * (↑p - 1)
H :
  ↑(Algebra.norm K) (↑(aeval ζ) (↑derivative (cyclotomic (↑p ^ (k + 1)) K))) = ↑↑p ^ (↑p ^ k * pred (succ k * (↑p - 1)))
⊢ ↑(Algebra.norm K) (↑(aeval ζ) (↑derivative (cyclotomic (↑p ^ (k + 1)) K))) =
    ↑↑(p ^ (↑p ^ k * ((↑p - 1) * (k + 1) - 1)))
[PROOFSTEP]
simp only [H, mul_comm _ (k + 1)]
[GOAL]
case e_a.refine_2
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑↑(p ^ (k + 1))
mf : Module.Finite K L
se : IsSeparable K L
coe_two : ↑2 = 2
hp2 : p = 2 → k ≠ 0
hnorm : ↑(Algebra.norm K) (ζ ^ ↑p ^ k - 1) = ↑↑p ^ ↑p ^ k
this : 0 < succ k * (↑p - 1)
H :
  ↑(Algebra.norm K) (↑(aeval ζ) (↑derivative (cyclotomic (↑p ^ (k + 1)) K))) = ↑↑p ^ (↑p ^ k * pred (succ k * (↑p - 1)))
⊢ ↑↑p ^ (↑p ^ k * pred (succ k * (↑p - 1))) = ↑↑(p ^ (↑p ^ k * ((k + 1) * (↑p - 1) - 1)))
[PROOFSTEP]
norm_cast
[GOAL]
case e_a.refine_1
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑↑(p ^ (k + 1))
mf : Module.Finite K L
se : IsSeparable K L
coe_two : ↑2 = 2
hp2 : p = 2 → k ≠ 0
H :
  ↑(Algebra.norm K) (↑(aeval ζ) (↑derivative (cyclotomic (↑p ^ (k + 1)) K))) * ↑↑p ^ ↑p ^ k =
    ↑↑p ^ (↑p ^ k * pred (succ k * (↑p - 1))) * ↑↑p ^ ↑p ^ k
hnorm : ↑(Algebra.norm K) (ζ ^ ↑p ^ k - 1) = ↑↑p ^ ↑p ^ k
this : 0 < succ k * (↑p - 1)
h : ↑↑p ^ ↑p ^ k = 0
⊢ False
[PROOFSTEP]
have := hne.1
[GOAL]
case e_a.refine_1
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑↑(p ^ (k + 1))
mf : Module.Finite K L
se : IsSeparable K L
coe_two : ↑2 = 2
hp2 : p = 2 → k ≠ 0
H :
  ↑(Algebra.norm K) (↑(aeval ζ) (↑derivative (cyclotomic (↑p ^ (k + 1)) K))) * ↑↑p ^ ↑p ^ k =
    ↑↑p ^ (↑p ^ k * pred (succ k * (↑p - 1))) * ↑↑p ^ ↑p ^ k
hnorm : ↑(Algebra.norm K) (ζ ^ ↑p ^ k - 1) = ↑↑p ^ ↑p ^ k
this✝ : 0 < succ k * (↑p - 1)
h : ↑↑p ^ ↑p ^ k = 0
this : ↑↑(p ^ (k + 1)) ≠ 0
⊢ False
[PROOFSTEP]
rw [PNat.pow_coe, Nat.cast_pow, Ne.def, pow_eq_zero_iff (by linarith)] at this
[GOAL]
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑↑(p ^ (k + 1))
mf : Module.Finite K L
se : IsSeparable K L
coe_two : ↑2 = 2
hp2 : p = 2 → k ≠ 0
H :
  ↑(Algebra.norm K) (↑(aeval ζ) (↑derivative (cyclotomic (↑p ^ (k + 1)) K))) * ↑↑p ^ ↑p ^ k =
    ↑↑p ^ (↑p ^ k * pred (succ k * (↑p - 1))) * ↑↑p ^ ↑p ^ k
hnorm : ↑(Algebra.norm K) (ζ ^ ↑p ^ k - 1) = ↑↑p ^ ↑p ^ k
this✝ : 0 < succ k * (↑p - 1)
h : ↑↑p ^ ↑p ^ k = 0
this : ¬↑↑p ^ (k + 1) = 0
⊢ 0 < k + 1
[PROOFSTEP]
linarith
[GOAL]
case e_a.refine_1
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑↑(p ^ (k + 1))
mf : Module.Finite K L
se : IsSeparable K L
coe_two : ↑2 = 2
hp2 : p = 2 → k ≠ 0
H :
  ↑(Algebra.norm K) (↑(aeval ζ) (↑derivative (cyclotomic (↑p ^ (k + 1)) K))) * ↑↑p ^ ↑p ^ k =
    ↑↑p ^ (↑p ^ k * pred (succ k * (↑p - 1))) * ↑↑p ^ ↑p ^ k
hnorm : ↑(Algebra.norm K) (ζ ^ ↑p ^ k - 1) = ↑↑p ^ ↑p ^ k
this✝ : 0 < succ k * (↑p - 1)
h : ↑↑p ^ ↑p ^ k = 0
this : ¬↑↑p = 0
⊢ False
[PROOFSTEP]
exact absurd (pow_eq_zero h) this
[GOAL]
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hk : p ^ (k + 1) ≠ 2
⊢ discr K ↑(IsPrimitiveRoot.powerBasis K hζ).basis =
    ↑((-1) ^ (↑p ^ k * (↑p - 1) / 2)) * ↑↑(p ^ (↑p ^ k * ((↑p - 1) * (k + 1) - 1)))
[PROOFSTEP]
simpa [totient_prime_pow hp.out (succ_pos k)] using discr_prime_pow_ne_two hζ hirr hk
[GOAL]
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hcycl : IsCyclotomicExtension {p ^ k} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
hirr : Irreducible (cyclotomic (↑(p ^ k)) K)
⊢ discr K ↑(IsPrimitiveRoot.powerBasis K hζ).basis =
    ↑((-1) ^ (φ ↑(p ^ k) / 2)) * ↑↑(p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1)))
[PROOFSTEP]
cases' k with k k
[GOAL]
case zero
p : ℕ+
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ Nat.zero} K L
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.zero)
hirr : Irreducible (cyclotomic (↑(p ^ Nat.zero)) K)
⊢ discr K ↑(IsPrimitiveRoot.powerBasis K hζ).basis =
    ↑((-1) ^ (φ ↑(p ^ Nat.zero) / 2)) * ↑↑(p ^ (↑p ^ (Nat.zero - 1) * ((↑p - 1) * Nat.zero - 1)))
[PROOFSTEP]
simp only [coe_basis, _root_.pow_zero, powerBasis_gen _ hζ, totient_one, mul_zero, mul_one, show 1 / 2 = 0 by rfl,
  discr, traceMatrix]
[GOAL]
p : ℕ+
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ Nat.zero} K L
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.zero)
hirr : Irreducible (cyclotomic (↑(p ^ Nat.zero)) K)
⊢ 1 / 2 = 0
[PROOFSTEP]
rfl
[GOAL]
case zero
p : ℕ+
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ Nat.zero} K L
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.zero)
hirr : Irreducible (cyclotomic (↑(p ^ Nat.zero)) K)
⊢ Matrix.det (↑Matrix.of fun i j => BilinForm.bilin (traceForm K L) (ζ ^ ↑i) (ζ ^ ↑j)) =
    ↑((-1) ^ (φ ↑1 / 2)) * ↑↑(p ^ (↑p ^ (Nat.zero - 1) * ((↑p - 1) * Nat.zero - 1)))
[PROOFSTEP]
have hζone : ζ = 1 := by simpa using hζ
[GOAL]
p : ℕ+
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ Nat.zero} K L
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.zero)
hirr : Irreducible (cyclotomic (↑(p ^ Nat.zero)) K)
⊢ ζ = 1
[PROOFSTEP]
simpa using hζ
[GOAL]
case zero
p : ℕ+
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ Nat.zero} K L
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.zero)
hirr : Irreducible (cyclotomic (↑(p ^ Nat.zero)) K)
hζone : ζ = 1
⊢ Matrix.det (↑Matrix.of fun i j => BilinForm.bilin (traceForm K L) (ζ ^ ↑i) (ζ ^ ↑j)) =
    ↑((-1) ^ (φ ↑1 / 2)) * ↑↑(p ^ (↑p ^ (Nat.zero - 1) * ((↑p - 1) * Nat.zero - 1)))
[PROOFSTEP]
rw [hζ.powerBasis_dim _, hζone, ← (algebraMap K L).map_one,
  minpoly.eq_X_sub_C_of_algebraMap_inj _ (algebraMap K L).injective, natDegree_X_sub_C]
[GOAL]
case zero
p : ℕ+
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ Nat.zero} K L
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.zero)
hirr : Irreducible (cyclotomic (↑(p ^ Nat.zero)) K)
hζone : ζ = 1
⊢ Matrix.det
      (↑Matrix.of fun i j => BilinForm.bilin (traceForm K L) (↑(algebraMap K L) 1 ^ ↑i) (↑(algebraMap K L) 1 ^ ↑j)) =
    ↑((-1) ^ (φ ↑1 / 2)) * ↑↑(p ^ (↑p ^ (Nat.zero - 1) * ((↑p - 1) * Nat.zero - 1)))
[PROOFSTEP]
simp only [traceMatrix, map_one, one_pow, Matrix.det_unique, traceForm_apply, mul_one]
[GOAL]
case zero
p : ℕ+
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ Nat.zero} K L
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.zero)
hirr : Irreducible (cyclotomic (↑(p ^ Nat.zero)) K)
hζone : ζ = 1
⊢ ↑Matrix.of (fun i j => ↑(trace K L) 1) default default =
    ↑((-1) ^ (φ ↑1 / 2)) * ↑↑(p ^ (↑p ^ (Nat.zero - 1) * ((↑p - 1) * Nat.zero - 1)))
[PROOFSTEP]
rw [← (algebraMap K L).map_one, trace_algebraMap, finrank _ hirr]
[GOAL]
case zero
p : ℕ+
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ Nat.zero} K L
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.zero)
hirr : Irreducible (cyclotomic (↑(p ^ Nat.zero)) K)
hζone : ζ = 1
⊢ ↑Matrix.of (fun i j => φ ↑(p ^ Nat.zero) • 1) default default =
    ↑((-1) ^ (φ ↑1 / 2)) * ↑↑(p ^ (↑p ^ (Nat.zero - 1) * ((↑p - 1) * Nat.zero - 1)))
[PROOFSTEP]
norm_num
[GOAL]
case succ
p : ℕ+
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime ↑p)
k : ℕ
hcycl : IsCyclotomicExtension {p ^ succ k} K L
hζ : IsPrimitiveRoot ζ ↑(p ^ succ k)
hirr : Irreducible (cyclotomic (↑(p ^ succ k)) K)
⊢ discr K ↑(IsPrimitiveRoot.powerBasis K hζ).basis =
    ↑((-1) ^ (φ ↑(p ^ succ k) / 2)) * ↑↑(p ^ (↑p ^ (succ k - 1) * ((↑p - 1) * succ k - 1)))
[PROOFSTEP]
by_cases hk : p ^ (k + 1) = 2
[GOAL]
case pos
p : ℕ+
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime ↑p)
k : ℕ
hcycl : IsCyclotomicExtension {p ^ succ k} K L
hζ : IsPrimitiveRoot ζ ↑(p ^ succ k)
hirr : Irreducible (cyclotomic (↑(p ^ succ k)) K)
hk : p ^ (k + 1) = 2
⊢ discr K ↑(IsPrimitiveRoot.powerBasis K hζ).basis =
    ↑((-1) ^ (φ ↑(p ^ succ k) / 2)) * ↑↑(p ^ (↑p ^ (succ k - 1) * ((↑p - 1) * succ k - 1)))
[PROOFSTEP]
have coe_two : 2 = ((2 : ℕ+) : ℕ) := rfl
[GOAL]
case pos
p : ℕ+
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime ↑p)
k : ℕ
hcycl : IsCyclotomicExtension {p ^ succ k} K L
hζ : IsPrimitiveRoot ζ ↑(p ^ succ k)
hirr : Irreducible (cyclotomic (↑(p ^ succ k)) K)
hk : p ^ (k + 1) = 2
coe_two : 2 = ↑2
⊢ discr K ↑(IsPrimitiveRoot.powerBasis K hζ).basis =
    ↑((-1) ^ (φ ↑(p ^ succ k) / 2)) * ↑↑(p ^ (↑p ^ (succ k - 1) * ((↑p - 1) * succ k - 1)))
[PROOFSTEP]
have hp : p = 2 := by
  rw [← PNat.coe_inj, PNat.pow_coe, ← pow_one 2] at hk
  replace hk := eq_of_prime_pow_eq (prime_iff.1 hp.out) (prime_iff.1 Nat.prime_two) (succ_pos _) hk
  rwa [coe_two, PNat.coe_inj] at hk
[GOAL]
p : ℕ+
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime ↑p)
k : ℕ
hcycl : IsCyclotomicExtension {p ^ succ k} K L
hζ : IsPrimitiveRoot ζ ↑(p ^ succ k)
hirr : Irreducible (cyclotomic (↑(p ^ succ k)) K)
hk : p ^ (k + 1) = 2
coe_two : 2 = ↑2
⊢ p = 2
[PROOFSTEP]
rw [← PNat.coe_inj, PNat.pow_coe, ← pow_one 2] at hk
[GOAL]
p : ℕ+
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime ↑p)
k : ℕ
hcycl : IsCyclotomicExtension {p ^ succ k} K L
hζ : IsPrimitiveRoot ζ ↑(p ^ succ k)
hirr : Irreducible (cyclotomic (↑(p ^ succ k)) K)
hk✝ : ↑p ^ (k + 1) = ↑2
hk : ↑p ^ (k + 1) = ↑(2 ^ 1)
coe_two : 2 = ↑2
⊢ p = 2
[PROOFSTEP]
replace hk := eq_of_prime_pow_eq (prime_iff.1 hp.out) (prime_iff.1 Nat.prime_two) (succ_pos _) hk
[GOAL]
p : ℕ+
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime ↑p)
k : ℕ
hcycl : IsCyclotomicExtension {p ^ succ k} K L
hζ : IsPrimitiveRoot ζ ↑(p ^ succ k)
hirr : Irreducible (cyclotomic (↑(p ^ succ k)) K)
hk✝ : ↑p ^ (k + 1) = ↑2
coe_two : 2 = ↑2
hk : ↑p = 2
⊢ p = 2
[PROOFSTEP]
rwa [coe_two, PNat.coe_inj] at hk
[GOAL]
case pos
p : ℕ+
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp✝ : Fact (Nat.Prime ↑p)
k : ℕ
hcycl : IsCyclotomicExtension {p ^ succ k} K L
hζ : IsPrimitiveRoot ζ ↑(p ^ succ k)
hirr : Irreducible (cyclotomic (↑(p ^ succ k)) K)
hk : p ^ (k + 1) = 2
coe_two : 2 = ↑2
hp : p = 2
⊢ discr K ↑(IsPrimitiveRoot.powerBasis K hζ).basis =
    ↑((-1) ^ (φ ↑(p ^ succ k) / 2)) * ↑↑(p ^ (↑p ^ (succ k - 1) * ((↑p - 1) * succ k - 1)))
[PROOFSTEP]
rw [hp, ← PNat.coe_inj, PNat.pow_coe] at hk
[GOAL]
case pos
p : ℕ+
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp✝ : Fact (Nat.Prime ↑p)
k : ℕ
hcycl : IsCyclotomicExtension {p ^ succ k} K L
hζ : IsPrimitiveRoot ζ ↑(p ^ succ k)
hirr : Irreducible (cyclotomic (↑(p ^ succ k)) K)
hk : ↑2 ^ (k + 1) = ↑2
coe_two : 2 = ↑2
hp : p = 2
⊢ discr K ↑(IsPrimitiveRoot.powerBasis K hζ).basis =
    ↑((-1) ^ (φ ↑(p ^ succ k) / 2)) * ↑↑(p ^ (↑p ^ (succ k - 1) * ((↑p - 1) * succ k - 1)))
[PROOFSTEP]
nth_rw 2 [← pow_one 2] at hk
[GOAL]
case pos
p : ℕ+
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp✝ : Fact (Nat.Prime ↑p)
k : ℕ
hcycl : IsCyclotomicExtension {p ^ succ k} K L
hζ : IsPrimitiveRoot ζ ↑(p ^ succ k)
hirr : Irreducible (cyclotomic (↑(p ^ succ k)) K)
hk✝ : ↑2 ^ (k + 1) = ↑2
hk : ↑2 ^ (k + 1) = ↑(2 ^ 1)
coe_two : 2 = ↑2
hp : p = 2
⊢ discr K ↑(IsPrimitiveRoot.powerBasis K hζ).basis =
    ↑((-1) ^ (φ ↑(p ^ succ k) / 2)) * ↑↑(p ^ (↑p ^ (succ k - 1) * ((↑p - 1) * succ k - 1)))
[PROOFSTEP]
replace hk := Nat.pow_right_injective rfl.le hk
[GOAL]
case pos
p : ℕ+
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp✝ : Fact (Nat.Prime ↑p)
k : ℕ
hcycl : IsCyclotomicExtension {p ^ succ k} K L
hζ : IsPrimitiveRoot ζ ↑(p ^ succ k)
hirr : Irreducible (cyclotomic (↑(p ^ succ k)) K)
hk✝ : ↑2 ^ (k + 1) = ↑2
coe_two : 2 = ↑2
hp : p = 2
hk : k + 1 = 1
⊢ discr K ↑(IsPrimitiveRoot.powerBasis K hζ).basis =
    ↑((-1) ^ (φ ↑(p ^ succ k) / 2)) * ↑↑(p ^ (↑p ^ (succ k - 1) * ((↑p - 1) * succ k - 1)))
[PROOFSTEP]
rw [add_left_eq_self] at hk
[GOAL]
case pos
p : ℕ+
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp✝ : Fact (Nat.Prime ↑p)
k : ℕ
hcycl : IsCyclotomicExtension {p ^ succ k} K L
hζ : IsPrimitiveRoot ζ ↑(p ^ succ k)
hirr : Irreducible (cyclotomic (↑(p ^ succ k)) K)
hk✝ : ↑2 ^ (k + 1) = ↑2
coe_two : 2 = ↑2
hp : p = 2
hk : k = 0
⊢ discr K ↑(IsPrimitiveRoot.powerBasis K hζ).basis =
    ↑((-1) ^ (φ ↑(p ^ succ k) / 2)) * ↑↑(p ^ (↑p ^ (succ k - 1) * ((↑p - 1) * succ k - 1)))
[PROOFSTEP]
rw [hp, hk] at hζ
[GOAL]
case pos
p : ℕ+
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp✝ : Fact (Nat.Prime ↑p)
k : ℕ
hcycl : IsCyclotomicExtension {p ^ succ k} K L
hζ✝ : IsPrimitiveRoot ζ ↑(p ^ succ k)
hζ : IsPrimitiveRoot ζ ↑(2 ^ succ 0)
hirr : Irreducible (cyclotomic (↑(p ^ succ k)) K)
hk✝ : ↑2 ^ (k + 1) = ↑2
coe_two : 2 = ↑2
hp : p = 2
hk : k = 0
⊢ discr K ↑(IsPrimitiveRoot.powerBasis K hζ✝).basis =
    ↑((-1) ^ (φ ↑(p ^ succ k) / 2)) * ↑↑(p ^ (↑p ^ (succ k - 1) * ((↑p - 1) * succ k - 1)))
[PROOFSTEP]
norm_num at hζ
[GOAL]
case pos
p : ℕ+
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp✝ : Fact (Nat.Prime ↑p)
k : ℕ
hcycl : IsCyclotomicExtension {p ^ succ k} K L
hζ✝ : IsPrimitiveRoot ζ ↑(p ^ succ k)
hirr : Irreducible (cyclotomic (↑(p ^ succ k)) K)
hk✝ : ↑2 ^ (k + 1) = ↑2
coe_two : 2 = ↑2
hp : p = 2
hk : k = 0
hζ : IsPrimitiveRoot ζ ↑2
⊢ discr K ↑(IsPrimitiveRoot.powerBasis K hζ✝).basis =
    ↑((-1) ^ (φ ↑(p ^ succ k) / 2)) * ↑↑(p ^ (↑p ^ (succ k - 1) * ((↑p - 1) * succ k - 1)))
[PROOFSTEP]
rw [← coe_two] at hζ
[GOAL]
case pos
p : ℕ+
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp✝ : Fact (Nat.Prime ↑p)
k : ℕ
hcycl : IsCyclotomicExtension {p ^ succ k} K L
hζ✝ : IsPrimitiveRoot ζ ↑(p ^ succ k)
hirr : Irreducible (cyclotomic (↑(p ^ succ k)) K)
hk✝ : ↑2 ^ (k + 1) = ↑2
coe_two : 2 = ↑2
hp : p = 2
hk : k = 0
hζ : IsPrimitiveRoot ζ 2
⊢ discr K ↑(IsPrimitiveRoot.powerBasis K hζ✝).basis =
    ↑((-1) ^ (φ ↑(p ^ succ k) / 2)) * ↑↑(p ^ (↑p ^ (succ k - 1) * ((↑p - 1) * succ k - 1)))
[PROOFSTEP]
rw [coe_basis, powerBasis_gen]
[GOAL]
case pos
p : ℕ+
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp✝ : Fact (Nat.Prime ↑p)
k : ℕ
hcycl : IsCyclotomicExtension {p ^ succ k} K L
hζ✝ : IsPrimitiveRoot ζ ↑(p ^ succ k)
hirr : Irreducible (cyclotomic (↑(p ^ succ k)) K)
hk✝ : ↑2 ^ (k + 1) = ↑2
coe_two : 2 = ↑2
hp : p = 2
hk : k = 0
hζ : IsPrimitiveRoot ζ 2
⊢ (discr K fun i => ζ ^ ↑i) = ↑((-1) ^ (φ ↑(p ^ succ k) / 2)) * ↑↑(p ^ (↑p ^ (succ k - 1) * ((↑p - 1) * succ k - 1)))
[PROOFSTEP]
simp only [hp, hk]
[GOAL]
case pos
p : ℕ+
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp✝ : Fact (Nat.Prime ↑p)
k : ℕ
hcycl : IsCyclotomicExtension {p ^ succ k} K L
hζ✝ : IsPrimitiveRoot ζ ↑(p ^ succ k)
hirr : Irreducible (cyclotomic (↑(p ^ succ k)) K)
hk✝ : ↑2 ^ (k + 1) = ↑2
coe_two : 2 = ↑2
hp : p = 2
hk : k = 0
hζ : IsPrimitiveRoot ζ 2
⊢ (discr K fun i => ζ ^ ↑i) = ↑((-1) ^ (φ ↑(2 ^ succ 0) / 2)) * ↑↑(2 ^ (↑2 ^ (succ 0 - 1) * ((↑2 - 1) * succ 0 - 1)))
[PROOFSTEP]
norm_num
  -- Porting note: the goal at this point is `(discr K fun i ↦ ζ ^ ↑i) = 1`.
        -- This `simp_rw` is needed so the next `rw` can rewrite the type of `i` from
        -- `Fin (natDegree (minpoly K ζ))` to `Fin 1`
[GOAL]
case pos
p : ℕ+
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp✝ : Fact (Nat.Prime ↑p)
k : ℕ
hcycl : IsCyclotomicExtension {p ^ succ k} K L
hζ✝ : IsPrimitiveRoot ζ ↑(p ^ succ k)
hirr : Irreducible (cyclotomic (↑(p ^ succ k)) K)
hk✝ : ↑2 ^ (k + 1) = ↑2
coe_two : 2 = ↑2
hp : p = 2
hk : k = 0
hζ : IsPrimitiveRoot ζ 2
⊢ (discr K fun i => ζ ^ ↑i) = 1
[PROOFSTEP]
simp_rw [hζ.eq_neg_one_of_two_right, show (-1 : L) = algebraMap K L (-1) by simp]
[GOAL]
p : ℕ+
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp✝ : Fact (Nat.Prime ↑p)
k : ℕ
hcycl : IsCyclotomicExtension {p ^ succ k} K L
hζ✝ : IsPrimitiveRoot ζ ↑(p ^ succ k)
hirr : Irreducible (cyclotomic (↑(p ^ succ k)) K)
hk✝ : ↑2 ^ (k + 1) = ↑2
coe_two : 2 = ↑2
hp : p = 2
hk : k = 0
hζ : IsPrimitiveRoot ζ 2
⊢ -1 = ↑(algebraMap K L) (-1)
[PROOFSTEP]
simp
[GOAL]
case pos
p : ℕ+
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp✝ : Fact (Nat.Prime ↑p)
k : ℕ
hcycl : IsCyclotomicExtension {p ^ succ k} K L
hζ✝ : IsPrimitiveRoot ζ ↑(p ^ succ k)
hirr : Irreducible (cyclotomic (↑(p ^ succ k)) K)
hk✝ : ↑2 ^ (k + 1) = ↑2
coe_two : 2 = ↑2
hp : p = 2
hk : k = 0
hζ : IsPrimitiveRoot ζ 2
⊢ (discr K fun i => ↑(algebraMap K L) (-1) ^ ↑i) = 1
[PROOFSTEP]
rw [hζ.eq_neg_one_of_two_right, show (-1 : L) = algebraMap K L (-1) by simp,
  minpoly.eq_X_sub_C_of_algebraMap_inj _ (algebraMap K L).injective, natDegree_X_sub_C]
[GOAL]
p : ℕ+
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp✝ : Fact (Nat.Prime ↑p)
k : ℕ
hcycl : IsCyclotomicExtension {p ^ succ k} K L
hζ✝ : IsPrimitiveRoot ζ ↑(p ^ succ k)
hirr : Irreducible (cyclotomic (↑(p ^ succ k)) K)
hk✝ : ↑2 ^ (k + 1) = ↑2
coe_two : 2 = ↑2
hp : p = 2
hk : k = 0
hζ : IsPrimitiveRoot ζ 2
⊢ -1 = ↑(algebraMap K L) (-1)
[PROOFSTEP]
simp
[GOAL]
case pos
p : ℕ+
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp✝ : Fact (Nat.Prime ↑p)
k : ℕ
hcycl : IsCyclotomicExtension {p ^ succ k} K L
hζ✝ : IsPrimitiveRoot ζ ↑(p ^ succ k)
hirr : Irreducible (cyclotomic (↑(p ^ succ k)) K)
hk✝ : ↑2 ^ (k + 1) = ↑2
coe_two : 2 = ↑2
hp : p = 2
hk : k = 0
hζ : IsPrimitiveRoot ζ 2
⊢ (discr K fun i => ↑(algebraMap K L) (-1) ^ ↑i) = 1
[PROOFSTEP]
simp only [discr, traceMatrix_apply, Matrix.det_unique, Fin.default_eq_zero, Fin.val_zero, _root_.pow_zero,
  traceForm_apply, mul_one]
[GOAL]
case pos
p : ℕ+
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp✝ : Fact (Nat.Prime ↑p)
k : ℕ
hcycl : IsCyclotomicExtension {p ^ succ k} K L
hζ✝ : IsPrimitiveRoot ζ ↑(p ^ succ k)
hirr : Irreducible (cyclotomic (↑(p ^ succ k)) K)
hk✝ : ↑2 ^ (k + 1) = ↑2
coe_two : 2 = ↑2
hp : p = 2
hk : k = 0
hζ : IsPrimitiveRoot ζ 2
⊢ ↑(trace K L) 1 = 1
[PROOFSTEP]
rw [← (algebraMap K L).map_one, trace_algebraMap, finrank _ hirr, hp, hk]
[GOAL]
case pos
p : ℕ+
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp✝ : Fact (Nat.Prime ↑p)
k : ℕ
hcycl : IsCyclotomicExtension {p ^ succ k} K L
hζ✝ : IsPrimitiveRoot ζ ↑(p ^ succ k)
hirr : Irreducible (cyclotomic (↑(p ^ succ k)) K)
hk✝ : ↑2 ^ (k + 1) = ↑2
coe_two : 2 = ↑2
hp : p = 2
hk : k = 0
hζ : IsPrimitiveRoot ζ 2
⊢ φ ↑(2 ^ succ 0) • 1 = 1
[PROOFSTEP]
norm_num
[GOAL]
case pos
p : ℕ+
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp✝ : Fact (Nat.Prime ↑p)
k : ℕ
hcycl : IsCyclotomicExtension {p ^ succ k} K L
hζ✝ : IsPrimitiveRoot ζ ↑(p ^ succ k)
hirr : Irreducible (cyclotomic (↑(p ^ succ k)) K)
hk✝ : ↑2 ^ (k + 1) = ↑2
coe_two : 2 = ↑2
hp : p = 2
hk : k = 0
hζ : IsPrimitiveRoot ζ 2
⊢ ↑(φ ↑2) = 1
[PROOFSTEP]
simp [← coe_two]
[GOAL]
case neg
p : ℕ+
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime ↑p)
k : ℕ
hcycl : IsCyclotomicExtension {p ^ succ k} K L
hζ : IsPrimitiveRoot ζ ↑(p ^ succ k)
hirr : Irreducible (cyclotomic (↑(p ^ succ k)) K)
hk : ¬p ^ (k + 1) = 2
⊢ discr K ↑(IsPrimitiveRoot.powerBasis K hζ).basis =
    ↑((-1) ^ (φ ↑(p ^ succ k) / 2)) * ↑↑(p ^ (↑p ^ (succ k - 1) * ((↑p - 1) * succ k - 1)))
[PROOFSTEP]
exact discr_prime_pow_ne_two hζ hirr hk
[GOAL]
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ k} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
hirr : Irreducible (cyclotomic (↑(p ^ k)) K)
⊢ ∃ u n, discr K ↑(IsPrimitiveRoot.powerBasis K hζ).basis = ↑↑u * ↑↑(p ^ n)
[PROOFSTEP]
rw [discr_prime_pow hζ hirr]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ k} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
hirr : Irreducible (cyclotomic (↑(p ^ k)) K)
⊢ ∃ u n, ↑((-1) ^ (φ ↑(p ^ k) / 2)) * ↑↑(p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1))) = ↑↑u * ↑↑(p ^ n)
[PROOFSTEP]
by_cases heven : Even ((p ^ k : ℕ).totient / 2)
[GOAL]
case pos
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ k} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
hirr : Irreducible (cyclotomic (↑(p ^ k)) K)
heven : Even (φ ↑(p ^ k) / 2)
⊢ ∃ u n, ↑((-1) ^ (φ ↑(p ^ k) / 2)) * ↑↑(p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1))) = ↑↑u * ↑↑(p ^ n)
[PROOFSTEP]
refine' ⟨1, (p : ℕ) ^ (k - 1) * ((p - 1) * k - 1), by rw [heven.neg_one_pow]; norm_num⟩
[GOAL]
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ k} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
hirr : Irreducible (cyclotomic (↑(p ^ k)) K)
heven : Even (φ ↑(p ^ k) / 2)
⊢ ↑((-1) ^ (φ ↑(p ^ k) / 2)) * ↑↑(p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1))) =
    ↑↑1 * ↑↑(p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1)))
[PROOFSTEP]
rw [heven.neg_one_pow]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ k} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
hirr : Irreducible (cyclotomic (↑(p ^ k)) K)
heven : Even (φ ↑(p ^ k) / 2)
⊢ ↑1 * ↑↑(p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1))) = ↑↑1 * ↑↑(p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1)))
[PROOFSTEP]
norm_num
[GOAL]
case neg
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ k} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
hirr : Irreducible (cyclotomic (↑(p ^ k)) K)
heven : ¬Even (φ ↑(p ^ k) / 2)
⊢ ∃ u n, ↑((-1) ^ (φ ↑(p ^ k) / 2)) * ↑↑(p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1))) = ↑↑u * ↑↑(p ^ n)
[PROOFSTEP]
exact ⟨-1, (p : ℕ) ^ (k - 1) * ((p - 1) * k - 1), by rw [(odd_iff_not_even.2 heven).neg_one_pow]; norm_num⟩
[GOAL]
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ k} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
hirr : Irreducible (cyclotomic (↑(p ^ k)) K)
heven : ¬Even (φ ↑(p ^ k) / 2)
⊢ ↑((-1) ^ (φ ↑(p ^ k) / 2)) * ↑↑(p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1))) =
    ↑↑(-1) * ↑↑(p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1)))
[PROOFSTEP]
rw [(odd_iff_not_even.2 heven).neg_one_pow]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ k} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
hirr : Irreducible (cyclotomic (↑(p ^ k)) K)
heven : ¬Even (φ ↑(p ^ k) / 2)
⊢ ↑(-1) * ↑↑(p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1))) = ↑↑(-1) * ↑↑(p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1)))
[PROOFSTEP]
norm_num
[GOAL]
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑p
hirr : Irreducible (cyclotomic (↑p) K)
hodd : p ≠ 2
⊢ discr K ↑(IsPrimitiveRoot.powerBasis K hζ).basis = ↑((-1) ^ ((↑p - 1) / 2)) * ↑↑(p ^ (↑p - 2))
[PROOFSTEP]
have : IsCyclotomicExtension {p ^ (0 + 1)} K L :=
  by
  rw [zero_add, pow_one]
  infer_instance
[GOAL]
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑p
hirr : Irreducible (cyclotomic (↑p) K)
hodd : p ≠ 2
⊢ IsCyclotomicExtension {p ^ (0 + 1)} K L
[PROOFSTEP]
rw [zero_add, pow_one]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑p
hirr : Irreducible (cyclotomic (↑p) K)
hodd : p ≠ 2
⊢ IsCyclotomicExtension {p} K L
[PROOFSTEP]
infer_instance
[GOAL]
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑p
hirr : Irreducible (cyclotomic (↑p) K)
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ (0 + 1)} K L
⊢ discr K ↑(IsPrimitiveRoot.powerBasis K hζ).basis = ↑((-1) ^ ((↑p - 1) / 2)) * ↑↑(p ^ (↑p - 2))
[PROOFSTEP]
have hζ' : IsPrimitiveRoot ζ ↑(p ^ (0 + 1)) := by simpa using hζ
[GOAL]
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑p
hirr : Irreducible (cyclotomic (↑p) K)
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ (0 + 1)} K L
⊢ IsPrimitiveRoot ζ ↑(p ^ (0 + 1))
[PROOFSTEP]
simpa using hζ
[GOAL]
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑p
hirr : Irreducible (cyclotomic (↑p) K)
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ (0 + 1)} K L
hζ' : IsPrimitiveRoot ζ ↑(p ^ (0 + 1))
⊢ discr K ↑(IsPrimitiveRoot.powerBasis K hζ).basis = ↑((-1) ^ ((↑p - 1) / 2)) * ↑↑(p ^ (↑p - 2))
[PROOFSTEP]
convert discr_prime_pow_ne_two hζ' (by simpa [hirr]) (by simp [hodd]) using 2
[GOAL]
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑p
hirr : Irreducible (cyclotomic (↑p) K)
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ (0 + 1)} K L
hζ' : IsPrimitiveRoot ζ ↑(p ^ (0 + 1))
⊢ Irreducible (cyclotomic ↑(p ^ (0 + 1)) ?m.954125)
[PROOFSTEP]
simpa [hirr]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑p
hirr : Irreducible (cyclotomic (↑p) K)
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ (0 + 1)} K L
hζ' : IsPrimitiveRoot ζ ↑(p ^ (0 + 1))
⊢ p ^ (0 + 1) ≠ 2
[PROOFSTEP]
simp [hodd]
[GOAL]
case h.e'_3.h.e'_5
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑p
hirr : Irreducible (cyclotomic (↑p) K)
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ (0 + 1)} K L
hζ' : IsPrimitiveRoot ζ ↑(p ^ (0 + 1))
⊢ ↑((-1) ^ ((↑p - 1) / 2)) = ↑((-1) ^ (φ ↑(p ^ (0 + 1)) / 2))
[PROOFSTEP]
rw [zero_add, pow_one, totient_prime hp.out]
[GOAL]
case h.e'_3.h.e'_6
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑p
hirr : Irreducible (cyclotomic (↑p) K)
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ (0 + 1)} K L
hζ' : IsPrimitiveRoot ζ ↑(p ^ (0 + 1))
⊢ ↑↑(p ^ (↑p - 2)) = ↑↑(p ^ (↑p ^ 0 * ((↑p - 1) * (0 + 1) - 1)))
[PROOFSTEP]
rw [_root_.pow_zero, one_mul, zero_add, mul_one, Nat.sub_sub]