awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero.{u} (R := K) (↑(p ^ (k + 1)) : K)
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp2 : p = 2 → k ≠ 0
H :
  Eq.{u + 1} (α := K)
    ((Algebra.norm K : (a : L) → K)
        (HMul.hMul (α := L) ((aeval ζ : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K ζ) : K[X]) : L)
          (ζ ^ p ^ k - 1)) :
      K)
    ((Algebra.norm K : (a : L) → K) ((↑(p ^ (k + 1)) : L) * ζ ^ (p ^ (k + 1) - 1)) : K)
hnorm : (Algebra.norm K : (a : L) → K) (ζ ^ p ^ k - 1) = HPow.hPow (α := K) (↑p : K) (p ^ k)
H₁ :
  HMul.hMul (α := K)
      ((Algebra.norm K : (a : L) → K)
          ((aeval ζ : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K ζ) : K[X]) : L) :
        K)
      (HPow.hPow (α := K) (↑p : K) (p ^ k)) =
    HMul.hMul (β := K) (HPow.hPow (α := K) (↑(p ^ k.succ) : K) (p ^ k * (p - 1)))
      ((Algebra.norm K : (a : L) → K) (ζ ^ (p ^ k.succ - 1)) : K)
⊢ (Algebra.norm K : (a : L) → K) (ζ ^ p ^ k - 1) = HPow.hPow (α := K) (↑p : K) (p ^ k)

Tactic:
rw [map_mul, hnorm, map_mul, ← map_natCast (algebraMap K L),
      Algebra.norm_algebraMap, finrank L hirr, ← succ_eq_add_one,
      totient_prime_pow hp.out (succ_pos k), Nat.sub_one, Nat.pred_succ] at H

Premises used: Nat.succ_eq_add_one, Algebra.algebraMap, Nat.totient_prime_pow, IsCyclotomicExtension.finrank, map_mul, map_natCast, Nat.pred_succ, Nat.succ_pos, Nat.sub_one, Algebra.norm_algebraMap, Fact.out
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero.{u} (R := K) (↑(p ^ (k + 1)) : K)
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp2 : p = 2 → k ≠ 0
H :
  HMul.hMul (α := K)
      ((Algebra.norm K : (a : L) → K)
          ((aeval ζ : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K ζ) : K[X]) : L) :
        K)
      (HPow.hPow (α := K) (↑p : K) (p ^ k)) =
    HMul.hMul (β := K) (HPow.hPow (α := K) (↑(p ^ k.succ) : K) (p ^ k * (p - 1)))
      ((Algebra.norm K : (a : L) → K) (ζ ^ (p ^ k.succ - 1)) : K)
hnorm : (Algebra.norm K : (a : L) → K) (ζ ^ p ^ k - 1) = HPow.hPow (α := K) (↑p : K) (p ^ k)
⊢ HMul.hMul (α := K)
      ((Algebra.norm K : (a : L) → K)
          ((aeval ζ : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (cyclotomic (p ^ (k + 1)) K) : K[X]) : L) :
        K)
      (HPow.hPow (α := K) (↑p : K) (p ^ k)) =
    HPow.hPow (α := K) (↑p : K) (p ^ k * ((k + 1) * (p - 1)))

Tactic:
rw [← hζ.minpoly_eq_cyclotomic_of_irreducible hirr, map_pow, hζ.norm_eq_one hk hirr, one_pow,
      mul_one, cast_pow, ← pow_mul, ← mul_assoc, mul_comm (k + 1), mul_assoc] at H

Premises used: one_pow, mul_assoc, IsPrimitiveRoot.norm_eq_one, map_pow, pow_mul, IsPrimitiveRoot.minpoly_eq_cyclotomic_of_irreducible, HAdd.hAdd, mul_comm, Nat.cast_pow, mul_one, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero.{u} (R := K) (↑(p ^ (k + 1)) : K)
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp2 : p = 2 → k ≠ 0
H :
  HMul.hMul (α := K)
      ((Algebra.norm K : (a : L) → K)
          ((aeval ζ : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K ζ) : K[X]) : L) :
        K)
      (HPow.hPow (α := K) (↑p : K) (p ^ k)) =
    HMul.hMul (β := K) (HPow.hPow (α := K) (↑(p ^ k.succ) : K) (p ^ k * (p - 1)))
      ((Algebra.norm K : (a : L) → K) (ζ ^ (p ^ k.succ - 1)) : K)
hnorm : (Algebra.norm K : (a : L) → K) (ζ ^ p ^ k - 1) = HPow.hPow (α := K) (↑p : K) (p ^ k)
H₁ :
  HMul.hMul (α := K)
      ((Algebra.norm K : (a : L) → K)
          ((aeval ζ : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (cyclotomic (p ^ (k + 1)) K) : K[X]) : L) :
        K)
      (HPow.hPow (α := K) (↑p : K) (p ^ k)) =
    HPow.hPow (α := K) (↑p : K) (p ^ k * ((k + 1) * (p - 1)))
⊢ (Algebra.norm K : (a : L) → K) (ζ ^ p ^ k - 1) = HPow.hPow (α := K) (↑p : K) (p ^ k)

Tactic:
rw [← hζ.minpoly_eq_cyclotomic_of_irreducible hirr, map_pow, hζ.norm_eq_one hk hirr, one_pow,
      mul_one, cast_pow, ← pow_mul, ← mul_assoc, mul_comm (k + 1), mul_assoc] at H

Premises used: one_pow, mul_assoc, IsPrimitiveRoot.norm_eq_one, map_pow, pow_mul, IsPrimitiveRoot.minpoly_eq_cyclotomic_of_irreducible, HAdd.hAdd, mul_comm, Nat.cast_pow, mul_one, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero.{u} (R := K) (↑(p ^ (k + 1)) : K)
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp2 : p = 2 → k ≠ 0
H :
  HMul.hMul (α := K)
      ((Algebra.norm K : (a : L) → K)
          ((aeval ζ : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (cyclotomic (p ^ (k + 1)) K) : K[X]) : L) :
        K)
      (HPow.hPow (α := K) (↑p : K) (p ^ k)) =
    HPow.hPow (α := K) (↑p : K) (p ^ k * ((k + 1) * (p - 1)))
hnorm : (Algebra.norm K : (a : L) → K) (ζ ^ p ^ k - 1) = HPow.hPow (α := K) (↑p : K) (p ^ k)
⊢ 0 < k.succ * (p - 1)

Tactic:
have := mul_pos (succ_pos k) (tsub_pos_of_lt hp.out.one_lt)
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero.{u} (R := K) (↑(p ^ (k + 1)) : K)
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp2 : p = 2 → k ≠ 0
H :
  HMul.hMul (α := K)
      ((Algebra.norm K : (a : L) → K)
          ((aeval ζ : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (cyclotomic (p ^ (k + 1)) K) : K[X]) : L) :
        K)
      (HPow.hPow (α := K) (↑p : K) (p ^ k)) =
    HPow.hPow (α := K) (↑p : K) (p ^ k * ((k + 1) * (p - 1)))
hnorm : (Algebra.norm K : (a : L) → K) (ζ ^ p ^ k - 1) = HPow.hPow (α := K) (↑p : K) (p ^ k)
this : 0 < k.succ * (p - 1)
⊢ HMul.hMul (α := K)
      ((Algebra.norm K : (a : L) → K)
          ((aeval ζ : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (cyclotomic (p ^ (k + 1)) K) : K[X]) : L) :
        K)
      (HPow.hPow (α := K) (↑p : K) (p ^ k)) =
    HPow.hPow (α := K) (↑p : K) (p ^ k * (k.succ * (p - 1)).pred) * HPow.hPow (α := K) (↑p : K) (p ^ k)

Tactic:
rw [← succ_pred_eq_of_pos this, mul_succ, pow_add _ _ (p ^ k)] at H

Premises used: Nat.mul_succ, Nat.succ_pred_eq_of_pos, pow_add, HPow.hPow
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero.{u} (R := K) (↑(p ^ (k + 1)) : K)
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp2 : p = 2 → k ≠ 0
H :
  HMul.hMul (α := K)
      ((Algebra.norm K : (a : L) → K)
          ((aeval ζ : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (cyclotomic (p ^ (k + 1)) K) : K[X]) : L) :
        K)
      (HPow.hPow (α := K) (↑p : K) (p ^ k)) =
    HPow.hPow (α := K) (↑p : K) (p ^ k * ((k + 1) * (p - 1)))
hnorm : (Algebra.norm K : (a : L) → K) (ζ ^ p ^ k - 1) = HPow.hPow (α := K) (↑p : K) (p ^ k)
this : 0 < k.succ * (p - 1)
H₁ :
  HMul.hMul (α := K)
      ((Algebra.norm K : (a : L) → K)
          ((aeval ζ : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (cyclotomic (p ^ (k + 1)) K) : K[X]) : L) :
        K)
      (HPow.hPow (α := K) (↑p : K) (p ^ k)) =
    HPow.hPow (α := K) (↑p : K) (p ^ k * (k.succ * (p - 1)).pred) * HPow.hPow (α := K) (↑p : K) (p ^ k)
⊢ (Algebra.norm K : (a : L) → K) (ζ ^ p ^ k - 1) = HPow.hPow (α := K) (↑p : K) (p ^ k)

Tactic:
rw [← succ_pred_eq_of_pos this, mul_succ, pow_add _ _ (p ^ k)] at H

Premises used: Nat.mul_succ, Nat.succ_pred_eq_of_pos, pow_add, HPow.hPow
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero.{u} (R := K) (↑(p ^ (k + 1)) : K)
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp2 : p = 2 → k ≠ 0
H :
  HMul.hMul (α := K)
      ((Algebra.norm K : (a : L) → K)
          ((aeval ζ : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (cyclotomic (p ^ (k + 1)) K) : K[X]) : L) :
        K)
      (HPow.hPow (α := K) (↑p : K) (p ^ k)) =
    HPow.hPow (α := K) (↑p : K) (p ^ k * ((k + 1) * (p - 1)))
hnorm : (Algebra.norm K : (a : L) → K) (ζ ^ p ^ k - 1) = HPow.hPow (α := K) (↑p : K) (p ^ k)
this : 0 < k.succ * (p - 1)
H₁ :
  HMul.hMul (α := K)
      ((Algebra.norm K : (a : L) → K)
          ((aeval ζ : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (cyclotomic (p ^ (k + 1)) K) : K[X]) : L) :
        K)
      (HPow.hPow (α := K) (↑p : K) (p ^ k)) =
    HPow.hPow (α := K) (↑p : K) (p ^ k * (k.succ * (p - 1)).pred) * HPow.hPow (α := K) (↑p : K) (p ^ k)
hnorm₁ : (Algebra.norm K : (a : L) → K) (ζ ^ p ^ k - 1) = HPow.hPow (α := K) (↑p : K) (p ^ k)
⊢ 0 < k.succ * (p - 1)

Tactic:
rw [← succ_pred_eq_of_pos this, mul_succ, pow_add _ _ (p ^ k)] at H

Premises used: Nat.mul_succ, Nat.succ_pred_eq_of_pos, pow_add, HPow.hPow
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero.{u} (R := K) (↑(p ^ (k + 1)) : K)
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp2 : p = 2 → k ≠ 0
H :
  HMul.hMul (α := K)
      ((Algebra.norm K : (a : L) → K)
          ((aeval ζ : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (cyclotomic (p ^ (k + 1)) K) : K[X]) : L) :
        K)
      (HPow.hPow (α := K) (↑p : K) (p ^ k)) =
    HPow.hPow (α := K) (↑p : K) (p ^ k * (k.succ * (p - 1)).pred) * HPow.hPow (α := K) (↑p : K) (p ^ k)
hnorm : (Algebra.norm K : (a : L) → K) (ζ ^ p ^ k - 1) = HPow.hPow (α := K) (↑p : K) (p ^ k)
this : 0 < k.succ * (p - 1)
e_a :
  ∀
    (H :
      (Algebra.norm K : (a : L) → K)
          ((aeval ζ : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (cyclotomic (p ^ (k + 1)) K) : K[X]) : L) =
        HPow.hPow (α := K) (↑p : K) (p ^ k * (k.succ * (p - 1)).pred)),
    (Algebra.norm K : (a : L) → K)
        ((aeval ζ : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (cyclotomic (p ^ (k + 1)) K) : K[X]) : L) =
      HPow.hPow (α := K) (↑p : K) (p ^ k * ((p - 1) * (k + 1) - 1))
e_a₁ : ∀ (h : HPow.hPow (α := K) (↑p : K) (p ^ k) = 0), False
⊢ (Algebra.norm K : (a : L) → K)
      ((aeval ζ : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (cyclotomic (p ^ (k + 1)) K) : K[X]) : L) =
    HPow.hPow (α := K) (↑p : K) (p ^ k * ((p - 1) * (k + 1) - 1))

Tactic:
replace H := (mul_left_inj' fun h => ?_).1 H
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero.{u} (R := K) (↑(p ^ (k + 1)) : K)
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp2 : p = 2 → k ≠ 0
hnorm : (Algebra.norm K : (a : L) → K) (ζ ^ p ^ k - 1) = HPow.hPow (α := K) (↑p : K) (p ^ k)
this : 0 < k.succ * (p - 1)
H :
  (Algebra.norm K : (a : L) → K)
      ((aeval ζ : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (cyclotomic (p ^ (k + 1)) K) : K[X]) : L) =
    HPow.hPow (α := K) (↑p : K) (p ^ k * (k.succ * (p - 1)).pred)
e_a :
  HPow.hPow (α := K) (↑p : K) (p ^ k * (k.succ * (p - 1)).pred) =
    HPow.hPow (α := K) (↑p : K) (p ^ k * ((k + 1) * (p - 1) - 1))
⊢ (Algebra.norm K : (a : L) → K)
      ((aeval ζ : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (cyclotomic (p ^ (k + 1)) K) : K[X]) : L) =
    HPow.hPow (α := K) (↑p : K) (p ^ k * ((p - 1) * (k + 1) - 1))

Tactic:
simp only [H, mul_comm _ (k + 1)]

Premises used: HAdd.hAdd, mul_comm, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero.{u} (R := K) (↑(p ^ (k + 1)) : K)
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp2 : p = 2 → k ≠ 0
hnorm : (Algebra.norm K : (a : L) → K) (ζ ^ p ^ k - 1) = HPow.hPow (α := K) (↑p : K) (p ^ k)
this : 0 < k.succ * (p - 1)
H :
  (Algebra.norm K : (a : L) → K)
      ((aeval ζ : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (cyclotomic (p ^ (k + 1)) K) : K[X]) : L) =
    HPow.hPow (α := K) (↑p : K) (p ^ k * (k.succ * (p - 1)).pred)
e_a e_a₁ e_a₂ e_a₃ :
  Eq.{u + 1} (α := K) (↑(p ^ (p ^ k * (k.succ * (p - 1)).pred)) : K) (↑(p ^ (p ^ k * ((k + 1) * (p - 1) - 1))) : K)
⊢ HPow.hPow (α := K) (↑p : K) (p ^ k * (k.succ * (p - 1)).pred) =
    HPow.hPow (α := K) (↑p : K) (p ^ k * ((k + 1) * (p - 1) - 1))

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero.{u} (R := K) (↑(p ^ (k + 1)) : K)
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp2 : p = 2 → k ≠ 0
H :
  HMul.hMul (α := K)
      ((Algebra.norm K : (a : L) → K)
          ((aeval ζ : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (cyclotomic (p ^ (k + 1)) K) : K[X]) : L) :
        K)
      (HPow.hPow (α := K) (↑p : K) (p ^ k)) =
    HPow.hPow (α := K) (↑p : K) (p ^ k * (k.succ * (p - 1)).pred) * HPow.hPow (α := K) (↑p : K) (p ^ k)
hnorm : (Algebra.norm K : (a : L) → K) (ζ ^ p ^ k - 1) = HPow.hPow (α := K) (↑p : K) (p ^ k)
this : 0 < k.succ * (p - 1)
h : HPow.hPow (α := K) (↑p : K) (p ^ k) = 0
⊢ Ne.{u + 1} (α := K) (↑(p ^ (k + 1)) : K) 0

Tactic:
have := hne.1
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero.{u} (R := K) (↑(p ^ (k + 1)) : K)
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp2 : p = 2 → k ≠ 0
H :
  HMul.hMul (α := K)
      ((Algebra.norm K : (a : L) → K)
          ((aeval ζ : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (cyclotomic (p ^ (k + 1)) K) : K[X]) : L) :
        K)
      (HPow.hPow (α := K) (↑p : K) (p ^ k)) =
    HPow.hPow (α := K) (↑p : K) (p ^ k * (k.succ * (p - 1)).pred) * HPow.hPow (α := K) (↑p : K) (p ^ k)
hnorm : (Algebra.norm K : (a : L) → K) (ζ ^ p ^ k - 1) = HPow.hPow (α := K) (↑p : K) (p ^ k)
this_1 : 0 < k.succ * (p - 1)
h : HPow.hPow (α := K) (↑p : K) (p ^ k) = 0
this : ¬HPow.hPow (α := K) (↑p : K) (k + 1) = 0
⊢ k + 1 ≠ 0

Tactic:
lia
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero.{u} (R := K) (↑(p ^ (k + 1)) : K)
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp2 : p = 2 → k ≠ 0
H :
  HMul.hMul (α := K)
      ((Algebra.norm K : (a : L) → K)
          ((aeval ζ : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (cyclotomic (p ^ (k + 1)) K) : K[X]) : L) :
        K)
      (HPow.hPow (α := K) (↑p : K) (p ^ k)) =
    HPow.hPow (α := K) (↑p : K) (p ^ k * (k.succ * (p - 1)).pred) * HPow.hPow (α := K) (↑p : K) (p ^ k)
hnorm : (Algebra.norm K : (a : L) → K) (ζ ^ p ^ k - 1) = HPow.hPow (α := K) (↑p : K) (p ^ k)
this_1 : 0 < k.succ * (p - 1)
h : HPow.hPow (α := K) (↑p : K) (p ^ k) = 0
this : Ne.{u + 1} (α := K) (↑(p ^ (k + 1)) : K) 0
⊢ ¬Eq.{u + 1} (α := K) (↑p : K) 0

Tactic:
rw [Nat.cast_pow, Ne, pow_eq_zero_iff (by lia)] at this

Premises used: pow_eq_zero_iff, Ne, Nat.cast_pow
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero.{u} (R := K) (↑(p ^ (k + 1)) : K)
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp2 : p = 2 → k ≠ 0
H :
  HMul.hMul (α := K)
      ((Algebra.norm K : (a : L) → K)
          ((aeval ζ : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (cyclotomic (p ^ (k + 1)) K) : K[X]) : L) :
        K)
      (HPow.hPow (α := K) (↑p : K) (p ^ k)) =
    HPow.hPow (α := K) (↑p : K) (p ^ k * (k.succ * (p - 1)).pred) * HPow.hPow (α := K) (↑p : K) (p ^ k)
hnorm : (Algebra.norm K : (a : L) → K) (ζ ^ p ^ k - 1) = HPow.hPow (α := K) (↑p : K) (p ^ k)
this_1 : 0 < k.succ * (p - 1)
h : HPow.hPow (α := K) (↑p : K) (p ^ k) = 0
this : ¬Eq.{u + 1} (α := K) (↑p : K) 0
⊢ False

Tactic:
absurd (eq_zero_of_pow_eq_zero h) this

Premises used: absurd, eq_zero_of_pow_eq_zero
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero.{u} (R := K) (↑(p ^ (k + 1)) : K)
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp2 : p = 2 → k ≠ 0
H :
  HMul.hMul (α := K)
      ((Algebra.norm K : (a : L) → K)
          ((aeval ζ : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (cyclotomic (p ^ (k + 1)) K) : K[X]) : L) :
        K)
      (HPow.hPow (α := K) (↑p : K) (p ^ k)) =
    HPow.hPow (α := K) (↑p : K) (p ^ k * (k.succ * (p - 1)).pred) * HPow.hPow (α := K) (↑p : K) (p ^ k)
hnorm : (Algebra.norm K : (a : L) → K) (ζ ^ p ^ k - 1) = HPow.hPow (α := K) (↑p : K) (p ^ k)
this_1 : 0 < k.succ * (p - 1)
h : HPow.hPow (α := K) (↑p : K) (p ^ k) = 0
this : ¬Eq.{u + 1} (α := K) (↑p : K) 0
⊢ False

Tactic:
exact absurd (eq_zero_of_pow_eq_zero h) this

Premises used: absurd, eq_zero_of_pow_eq_zero
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
⊢ discr.{u, v, 0} (ι := Fin (dim (IsPrimitiveRoot.powerBasis K hζ))) K (B := L)
      (⇑(basis (IsPrimitiveRoot.powerBasis K hζ)) : (a : Fin (IsPrimitiveRoot.powerBasis K hζ).dim) → L) =
    HPow.hPow (α := K) (-1) (p ^ k * (p - 1) / 2) * HPow.hPow (α := K) (↑p : K) (p ^ k * ((p - 1) * (k + 1) - 1))

Tactic:
simpa [totient_prime_pow hp.out (succ_pos k)] using discr_prime_pow_ne_two hζ hirr hk

Premises used: Nat.totient_prime_pow, IsCyclotomicExtension.discr_prime_pow_ne_two, Nat.succ_pos, Fact.out
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
hcycl : IsCyclotomicExtension {p ^ k} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ k)
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ k) K)
zero :
  ∀ [hcycl : IsCyclotomicExtension {HPow.hPow (β := ℕ) p 0} K L] (hζ : IsPrimitiveRoot ζ (HPow.hPow (β := ℕ) p 0))
    (hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (β := ℕ) p 0) K)),
    discr.{u, v, 0} (ι := Fin (dim (IsPrimitiveRoot.powerBasis K hζ))) K (B := L)
        (⇑(basis (IsPrimitiveRoot.powerBasis K hζ)) : (a : Fin (IsPrimitiveRoot.powerBasis K hζ).dim) → L) =
      HPow.hPow (α := K) (-1) (φ (HPow.hPow (β := ℕ) p 0) / 2) *
        HPow.hPow (α := K) (↑p : K) (p ^ HSub.hSub (α := ℕ) 0 1 * ((p - 1) * 0 - 1))
succ :
  ∀ (k : ℕ) [hcycl : IsCyclotomicExtension {p ^ (k + 1)} K L] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1)))
    (hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)),
    discr.{u, v, 0} (ι := Fin (dim (IsPrimitiveRoot.powerBasis K hζ))) K (B := L)
        (⇑(basis (IsPrimitiveRoot.powerBasis K hζ)) : (a : Fin (IsPrimitiveRoot.powerBasis K hζ).dim) → L) =
      HPow.hPow (α := K) (-1) (φ (p ^ (k + 1)) / 2) *
        HPow.hPow (α := K) (↑p : K) (p ^ (k + 1 - 1) * ((p - 1) * (k + 1) - 1))
⊢ discr.{u, v, 0} (ι := Fin (dim (IsPrimitiveRoot.powerBasis K hζ))) K (B := L)
      (⇑(basis (IsPrimitiveRoot.powerBasis K hζ)) : (a : Fin (IsPrimitiveRoot.powerBasis K hζ).dim) → L) =
    HPow.hPow (α := K) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := K) (↑p : K) (p ^ (k - 1) * ((p - 1) * k - 1))

Tactic:
rcases k with - | k
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
hp : Fact (Nat.Prime p)
hcycl : IsCyclotomicExtension {HPow.hPow (β := ℕ) p 0} K L
hζ : IsPrimitiveRoot ζ (HPow.hPow (β := ℕ) p 0)
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (β := ℕ) p 0) K)
⊢ 1 / 2 = 0

Tactic:
rfl
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
hp : Fact (Nat.Prime p)
hcycl : IsCyclotomicExtension {HPow.hPow (β := ℕ) p 0} K L
hζ : IsPrimitiveRoot ζ (HPow.hPow (β := ℕ) p 0)
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (β := ℕ) p 0) K)
zero :
  Matrix.det (n := Fin (dim (IsPrimitiveRoot.powerBasis K hζ)))
      ((Matrix.of :
          (a : Fin (IsPrimitiveRoot.powerBasis K hζ).dim → Fin (IsPrimitiveRoot.powerBasis K hζ).dim → K) →
            Matrix (Fin (IsPrimitiveRoot.powerBasis K hζ).dim) (Fin (IsPrimitiveRoot.powerBasis K hζ).dim) K)
        fun (i j : Fin (dim (IsPrimitiveRoot.powerBasis K hζ))) ↦
        (((traceForm K L : (a : L) → L →ₗ[K] K) (ζ ^ (↑i : ℕ)) : L →ₗ[K] K) : (a : L) → K) (ζ ^ (↑j : ℕ))) =
    1 * HPow.hPow (α := K) (↑p : K) (p ^ HSub.hSub (α := ℕ) 0 1 * HSub.hSub (α := ℕ) 0 1)
⊢ discr.{u, v, 0} (ι := Fin (dim (IsPrimitiveRoot.powerBasis K hζ))) K (B := L)
      (⇑(basis (IsPrimitiveRoot.powerBasis K hζ)) : (a : Fin (IsPrimitiveRoot.powerBasis K hζ).dim) → L) =
    HPow.hPow (α := K) (-1) (φ (HPow.hPow (β := ℕ) p 0) / 2) *
      HPow.hPow (α := K) (↑p : K) (p ^ HSub.hSub (α := ℕ) 0 1 * ((p - 1) * 0 - 1))

Tactic:
simp only [coe_basis, _root_.pow_zero, powerBasis_gen _ hζ, totient_one, mul_zero,
      show 1 / 2 = 0 by rfl, discr, traceMatrix]

Premises used: PowerBasis.coe_basis, IsPrimitiveRoot.powerBasis_gen, pow_zero, MulZeroClass.mul_zero, Algebra.traceMatrix, Algebra.discr, Nat.totient_one