awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (goal)
Goal:
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl_1 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ_1 : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)) K)
this : natDegree (minpoly K ζ) = 1
⊢ discr.{u, v, 0} (ι := Fin (dim (IsPrimitiveRoot.powerBasis K hζ_1))) K (B := L)
      (⇑(basis (IsPrimitiveRoot.powerBasis K hζ_1)) : (a : Fin (IsPrimitiveRoot.powerBasis K hζ_1).dim) → L) =
    HPow.hPow (α := K) (-1) (φ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)) / 2) *
      HPow.hPow (α := K) (↑2 : K)
        (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1 - 1) * (HSub.hSub (α := ℕ) 2 1 * HAdd.hAdd (α := ℕ) 0 1 - 1))
have pos : ∀ (e : Fin (natDegree (minpoly K ζ)) ≃ Fin 1),
  discr.{u, v, 0} (ι := Fin (dim (IsPrimitiveRoot.powerBasis K hζ_1))) K (B := L)
      (⇑(basis (IsPrimitiveRoot.powerBasis K hζ_1)) : (a : Fin (IsPrimitiveRoot.powerBasis K hζ_1).dim) → L) =
    HPow.hPow (α := K) (-1) (φ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)) / 2) *
      HPow.hPow (α := K) (↑2 : K)
        (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1 - 1) * (HSub.hSub (α := ℕ) 2 1 * HAdd.hAdd (α := ℕ) 0 1 - 1))
Tactic: rcases Fin.equiv_iff_eq.2 this with ⟨e⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (goal)
Goal:
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl_1 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ_1 : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)) K)
this : natDegree (minpoly K ζ) = 1
e : Fin (natDegree (minpoly K ζ)) ≃ Fin 1
⊢ discr.{u, v, 0} (ι := Fin (dim (IsPrimitiveRoot.powerBasis K hζ_1))) K (B := L)
      (⇑(basis (IsPrimitiveRoot.powerBasis K hζ_1)) : (a : Fin (IsPrimitiveRoot.powerBasis K hζ_1).dim) → L) =
    HPow.hPow (α := K) (-1) (φ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)) / 2) *
      HPow.hPow (α := K) (↑2 : K)
        (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1 - 1) * (HSub.hSub (α := ℕ) 2 1 * HAdd.hAdd (α := ℕ) 0 1 - 1))
have pos : discr.{u, v, 0} (ι := Fin 1) K (B := L)
    ((fun (i : Fin (dim (IsPrimitiveRoot.powerBasis K hζ))) ↦ ζ ^ (↑i : ℕ)) ∘
      (⇑e.symm : (a : Fin 1) → Fin (IsPrimitiveRoot.powerBasis K hζ).dim)) =
  HPow.hPow (α := K) (-1) (φ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)) / 2) *
    HPow.hPow (α := K) (↑2 : K)
      (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1 - 1) * (HSub.hSub (α := ℕ) 2 1 * HAdd.hAdd (α := ℕ) 0 1 - 1))
Tactic: rw [← Algebra.discr_reindex K (hζ.powerBasis K).basis e, coe_basis, powerBasis_gen]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (goal)
Goal:
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl_1 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ_1 : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)) K)
this : natDegree (minpoly K ζ) = 1
e : Fin (natDegree (minpoly K ζ)) ≃ Fin 1
⊢ discr.{u, v, 0} (ι := Fin 1) K (B := L)
      ((fun (i : Fin (dim (IsPrimitiveRoot.powerBasis K hζ))) ↦ ζ ^ (↑i : ℕ)) ∘
        (⇑e.symm : (a : Fin 1) → Fin (IsPrimitiveRoot.powerBasis K hζ).dim)) =
    HPow.hPow (α := K) (-1) (φ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)) / 2) *
      HPow.hPow (α := K) (↑2 : K)
        (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1 - 1) * (HSub.hSub (α := ℕ) 2 1 * HAdd.hAdd (α := ℕ) 0 1 - 1))
have pos : discr.{u, v, 0} (ι := Fin 1) K (B := L)
    ((fun (i : Fin (natDegree (minpoly K ζ))) ↦ ζ ^ (↑i : ℕ)) ∘ (⇑e.symm : (a : Fin 1) → Fin (minpoly K ζ).natDegree)) =
  1
Tactic: simp only [powerBasis_dim,
        zero_add, pow_one, totient_two, reduceDiv, pow_zero, cast_ofNat, tsub_self,
        Nat.add_one_sub_one, mul_one, mul_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (goal)
Goal:
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl_1 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ_1 : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)) K)
this : natDegree (minpoly K ζ) = 1
e : Fin (natDegree (minpoly K ζ)) ≃ Fin 1
⊢ discr.{u, v, 0} (ι := Fin 1) K (B := L)
      ((fun (i : Fin (natDegree (minpoly K ζ))) ↦ ζ ^ (↑i : ℕ)) ∘
        (⇑e.symm : (a : Fin 1) → Fin (minpoly K ζ).natDegree)) =
    1
have pos : discr.{u, v, 0} (ι := Fin 1) K (B := L)
    ((fun (i : Fin (natDegree (minpoly K ζ))) ↦ HPow.hPow (α := L) ((algebraMap K L : (a : K) → L) (-1) : L) (↑i : ℕ)) ∘
      (⇑e.symm : (a : Fin 1) → Fin (minpoly K ζ).natDegree)) =
  1
Tactic: simp_rw [hζ.eq_neg_one_of_two_right, show (-1 : L) = algebraMap K L (-1) by simp]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (goal)
Goal:
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl_1 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ_1 : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)) K)
this : natDegree (minpoly K ζ) = 1
e : Fin (natDegree (minpoly K ζ)) ≃ Fin 1
⊢ discr.{u, v, 0} (ι := Fin 1) K (B := L)
      ((fun (i : Fin (natDegree (minpoly K ζ))) ↦
          HPow.hPow (α := L) ((algebraMap K L : (a : K) → L) (-1) : L) (↑i : ℕ)) ∘
        (⇑e.symm : (a : Fin 1) → Fin (minpoly K ζ).natDegree)) =
    1
have h : discr.{u, v, 0} (ι := Fin 1) K (B := L)
    ((fun (i : Fin (natDegree (minpoly K ζ))) ↦ HPow.hPow (α := L) ((algebraMap K L : (a : K) → L) (-1) : L) (↑i : ℕ)) ∘
      (⇑e.symm : (a : Fin 1) → Fin (minpoly K ζ).natDegree)) =
  discr.{u, v, 0} K (B := L) fun (i : Fin 1) ↦ HPow.hPow (α := L) ((algebraMap K L : (a : K) → L) (-1) : L) (↑i : ℕ)
Tactic: convert_to (discr K fun i : Fin 1 ↦ (algebraMap K L) (-1) ^ ↑i) = _
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (goal)
Goal:
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl_1 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ_1 : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)) K)
this : natDegree (minpoly K ζ) = 1
e : Fin (natDegree (minpoly K ζ)) ≃ Fin 1
h :
  discr.{u, v, 0} (ι := Fin 1) K (B := L)
      ((fun (i : Fin (natDegree (minpoly K ζ))) ↦
          HPow.hPow (α := L) ((algebraMap K L : (a : K) → L) (-1) : L) (↑i : ℕ)) ∘
        (⇑e.symm : (a : Fin 1) → Fin (minpoly K ζ).natDegree)) =
    discr.{u, v, 0} K (B := L) fun (i : Fin 1) ↦ HPow.hPow (α := L) ((algebraMap K L : (a : K) → L) (-1) : L) (↑i : ℕ)
⊢ discr.{u, v, 0} (ι := Fin 1) K (B := L)
      ((fun (i : Fin (natDegree (minpoly K ζ))) ↦
          HPow.hPow (α := L) ((algebraMap K L : (a : K) → L) (-1) : L) (↑i : ℕ)) ∘
        (⇑e.symm : (a : Fin 1) → Fin (minpoly K ζ).natDegree)) =
    1
have pos : (discr.{u, v, 0} K (B := L) fun (i : Fin 1) ↦ HPow.hPow (α := L) ((algebraMap K L : (a : K) → L) (-1) : L) (↑i : ℕ)) = 1
Tactic: convert_to (discr K fun i : Fin 1 ↦ (algebraMap K L) (-1) ^ ↑i) = _
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (goal)
Goal:
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl_1 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ_1 : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)) K)
this : natDegree (minpoly K ζ) = 1
e : Fin (natDegree (minpoly K ζ)) ≃ Fin 1
⊢ discr.{u, v, 0} (ι := Fin 1) K (B := L)
      ((fun (i : Fin (natDegree (minpoly K ζ))) ↦
          HPow.hPow (α := L) ((algebraMap K L : (a : K) → L) (-1) : L) (↑i : ℕ)) ∘
        (⇑e.symm : (a : Fin 1) → Fin (minpoly K ζ).natDegree)) =
    discr.{u, v, 0} K (B := L) fun (i : Fin 1) ↦ HPow.hPow (α := L) ((algebraMap K L : (a : K) → L) (-1) : L) (↑i : ℕ)
have h : Eq.{v + 1} (α := Fin 1 → L)
  ((fun (i : Fin (natDegree (minpoly K ζ))) ↦ HPow.hPow (α := L) ((algebraMap K L : (a : K) → L) (-1) : L) (↑i : ℕ)) ∘
    (⇑e.symm : (a : Fin 1) → Fin (minpoly K ζ).natDegree))
  fun (i : Fin 1) ↦ HPow.hPow (α := L) ((algebraMap K L : (a : K) → L) (-1) : L) (↑i : ℕ)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (goal)
Goal:
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl_1 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ_1 : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)) K)
this : natDegree (minpoly K ζ) = 1
e : Fin (natDegree (minpoly K ζ)) ≃ Fin 1
⊢ Eq.{v + 1} (α := Fin 1 → L)
    ((fun (i : Fin (natDegree (minpoly K ζ))) ↦ HPow.hPow (α := L) ((algebraMap K L : (a : K) → L) (-1) : L) (↑i : ℕ)) ∘
      (⇑e.symm : (a : Fin 1) → Fin (minpoly K ζ).natDegree))
    fun (i : Fin 1) ↦ HPow.hPow (α := L) ((algebraMap K L : (a : K) → L) (-1) : L) (↑i : ℕ)
have h : ∀ (i : Fin 1),
  ((fun (i : Fin (natDegree (minpoly K ζ))) ↦ HPow.hPow (α := L) ((algebraMap K L : (a : K) → L) (-1) : L) (↑i : ℕ)) ∘
        (⇑e.symm : (a : Fin 1) → Fin (minpoly K ζ).natDegree))
      i =
    HPow.hPow (α := L) ((algebraMap K L : (a : K) → L) (-1) : L) (↑i : ℕ)
Tactic: ext i
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (goal)
Goal:
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl_1 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ_1 : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)) K)
this : natDegree (minpoly K ζ) = 1
e : Fin (natDegree (minpoly K ζ)) ≃ Fin 1
i : Fin 1
⊢ ((fun (i : Fin (natDegree (minpoly K ζ))) ↦ HPow.hPow (α := L) ((algebraMap K L : (a : K) → L) (-1) : L) (↑i : ℕ)) ∘
        (⇑e.symm : (a : Fin 1) → Fin (minpoly K ζ).natDegree))
      i =
    HPow.hPow (α := L) ((algebraMap K L : (a : K) → L) (-1) : L) (↑i : ℕ)
have h : HPow.hPow (α := L) (-1) (↑((e.symm : (a : Fin 1) → Fin (minpoly K ζ).natDegree) i) : ℕ) = 1
Tactic: simp only [map_neg, map_one, Function.comp_apply, Fin.val_eq_zero, _root_.pow_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (goal)
Goal:
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl_1 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ_1 : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)) K)
this : natDegree (minpoly K ζ) = 1
e : Fin (natDegree (minpoly K ζ)) ≃ Fin 1
i : Fin 1
⊢ HPow.hPow (α := L) (-1) (↑((e.symm : (a : Fin 1) → Fin (minpoly K ζ).natDegree) i) : ℕ) = 1
have h : (↑((e.symm : (a : Fin 1) → Fin (minpoly K ζ).natDegree) i) : ℕ) = 0
Tactic: suffices (e.symm i : ℕ) = 0 by simp [this]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (goal)
Goal:
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl_1 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ_1 : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)) K)
this : natDegree (minpoly K ζ) = 1
e : Fin (natDegree (minpoly K ζ)) ≃ Fin 1
i : Fin 1
⊢ (↑((e.symm : (a : Fin 1) → Fin (minpoly K ζ).natDegree) i) : ℕ) = 0
have h : (↑((e.symm : (a : Fin 1) → Fin (minpoly K ζ).natDegree) i) : ℕ) < 1
Tactic: rw [← Nat.lt_one_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (goal)
Goal:
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl_1 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ_1 : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)) K)
this : natDegree (minpoly K ζ) = 1
e : Fin (natDegree (minpoly K ζ)) ≃ Fin 1
i : Fin 1
⊢ (↑((e.symm : (a : Fin 1) → Fin (minpoly K ζ).natDegree) i) : ℕ) < 1
have h : 1 = natDegree (minpoly K ζ)
Tactic: convert! (e.symm i).2
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (goal)
Goal:
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl_1 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ_1 : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)) K)
this : natDegree (minpoly K ζ) = 1
e : Fin (natDegree (minpoly K ζ)) ≃ Fin 1
i : Fin 1
⊢ 1 = natDegree (minpoly K ζ)
have h : Eq (α := ℕ) 1 1
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (goal)
Goal:
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl_1 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ_1 : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)) K)
this : natDegree (minpoly K ζ) = 1
e : Fin (natDegree (minpoly K ζ)) ≃ Fin 1
⊢ (discr.{u, v, 0} K (B := L) fun (i : Fin 1) ↦ HPow.hPow (α := L) ((algebraMap K L : (a : K) → L) (-1) : L) (↑i : ℕ)) =
    1
have pos : Eq.{u + 1} (α := K) ((trace K L : (a : L) → K) 1 : K) (1 : K)
Tactic: simp only [discr, traceMatrix_apply, Matrix.det_unique, Fin.default_eq_zero, Fin.val_zero,
          _root_.pow_zero, traceForm_apply, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (goal)
Goal:
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl_1 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ_1 : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)) K)
this : natDegree (minpoly K ζ) = 1
e : Fin (natDegree (minpoly K ζ)) ≃ Fin 1
⊢ Eq.{u + 1} (α := K) ((trace K L : (a : L) → K) 1 : K) (1 : K)
have pos : HSMul.hSMul (β := K) (φ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1))) 1 = 1
Tactic: rw [← (algebraMap K L).map_one, trace_algebraMap, finrank _ hirr]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (goal)
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} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ k)
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ k) K)
⊢ ∃ (u : ℤˣ) (n : ℕ),
    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) =
      (↑(↑u : ℤ) : K) * HPow.hPow (α := K) (↑p : K) n
have rw : ∃ (u : ℤˣ) (n : ℕ),
  HPow.hPow (α := K) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := K) (↑p : K) (p ^ (k - 1) * ((p - 1) * k - 1)) =
    (↑(↑u : ℤ) : K) * HPow.hPow (α := K) (↑p : K) n
Tactic: rw [discr_prime_pow hζ hirr]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (goal)
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} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ k)
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ k) K)
⊢ ∃ (u : ℤˣ) (n : ℕ),
    HPow.hPow (α := K) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := K) (↑p : K) (p ^ (k - 1) * ((p - 1) * k - 1)) =
      (↑(↑u : ℤ) : K) * HPow.hPow (α := K) (↑p : K) n
have pos : ∀ (heven : Even (φ (p ^ k) / 2)),
  ∃ (u : ℤˣ) (n : ℕ),
    HPow.hPow (α := K) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := K) (↑p : K) (p ^ (k - 1) * ((p - 1) * k - 1)) =
      (↑(↑u : ℤ) : K) * HPow.hPow (α := K) (↑p : K) n
Tactic: by_cases heven : Even ((p ^ k).totient / 2)
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (goal)
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} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ k)
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ k) K)
pos :
  ∀ (heven : Even (φ (p ^ k) / 2)),
    ∃ (u : ℤˣ) (n : ℕ),
      HPow.hPow (α := K) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := K) (↑p : K) (p ^ (k - 1) * ((p - 1) * k - 1)) =
        (↑(↑u : ℤ) : K) * HPow.hPow (α := K) (↑p : K) n
⊢ ∃ (u : ℤˣ) (n : ℕ),
    HPow.hPow (α := K) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := K) (↑p : K) (p ^ (k - 1) * ((p - 1) * k - 1)) =
      (↑(↑u : ℤ) : K) * HPow.hPow (α := K) (↑p : K) n
have neg : ∀ (heven : ¬Even (φ (p ^ k) / 2)),
  ∃ (u : ℤˣ) (n : ℕ),
    HPow.hPow (α := K) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := K) (↑p : K) (p ^ (k - 1) * ((p - 1) * k - 1)) =
      (↑(↑u : ℤ) : K) * HPow.hPow (α := K) (↑p : K) n
Tactic: by_cases heven : Even ((p ^ k).totient / 2)
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (goal)
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} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ k)
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ k) K)
heven : Even (φ (p ^ k) / 2)
⊢ HPow.hPow (α := K) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := K) (↑p : K) (p ^ (k - 1) * ((p - 1) * k - 1)) =
    (↑(↑1 : ℤ) : K) * HPow.hPow (α := K) (↑p : K) (p ^ (k - 1) * ((p - 1) * k - 1))
have rw : 1 * HPow.hPow (α := K) (↑p : K) (p ^ (k - 1) * ((p - 1) * k - 1)) =
  (↑(↑1 : ℤ) : K) * HPow.hPow (α := K) (↑p : K) (p ^ (k - 1) * ((p - 1) * k - 1))
Tactic: rw [heven.neg_one_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (goal)
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} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ k)
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ k) K)
heven : ¬Even (φ (p ^ k) / 2)
⊢ HPow.hPow (α := K) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := K) (↑p : K) (p ^ (k - 1) * ((p - 1) * k - 1)) =
    (↑(↑(-1) : ℤ) : K) * HPow.hPow (α := K) (↑p : K) (p ^ (k - 1) * ((p - 1) * k - 1))
have rw : -1 * HPow.hPow (α := K) (↑p : K) (p ^ (k - 1) * ((p - 1) * k - 1)) =
  (↑(↑(-1) : ℤ) : K) * HPow.hPow (α := K) (↑p : K) (p ^ (k - 1) * ((p - 1) * k - 1))
Tactic: rw [(not_even_iff_odd.1 heven).neg_one_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (hypothesis)
Goal:
p : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ p
hirr : Irreducible (M := K[X]) (cyclotomic p K)
hodd : p ≠ 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 - 1) / 2) * HPow.hPow (α := K) (↑p : K) (p - 2)
have this : IsCyclotomicExtension {p ^ HAdd.hAdd (α := ℕ) 0 1} K L
Tactic: have : IsCyclotomicExtension {p ^ (0 + 1)} K L := by
    rw [zero_add, pow_one]
    infer_instance
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (hypothesis)
Goal:
p : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ p
hirr : Irreducible (M := K[X]) (cyclotomic p K)
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ HAdd.hAdd (α := ℕ) 0 1} K L
⊢ 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 - 1) / 2) * HPow.hPow (α := K) (↑p : K) (p - 2)
have hζ' : IsPrimitiveRoot ζ (p ^ HAdd.hAdd (α := ℕ) 0 1)
Tactic: have hζ' : IsPrimitiveRoot ζ (p ^ (0 + 1)) := by simpa using hζ
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (goal)
Goal:
p : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ p
hirr : Irreducible (M := K[X]) (cyclotomic p K)
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ HAdd.hAdd (α := ℕ) 0 1} K L
hζ' : IsPrimitiveRoot ζ (p ^ HAdd.hAdd (α := ℕ) 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) ((p - 1) / 2) * HPow.hPow (α := K) (↑p : K) (p - 2)
have h : HPow.hPow (α := K) (-1) ((p - 1) / 2) = HPow.hPow (α := K) (-1) (φ (p ^ HAdd.hAdd (α := ℕ) 0 1) / 2)
Tactic: convert! discr_prime_pow_ne_two hζ' (by simpa [hirr]) (by simp [hodd]) using 2
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (goal)
Goal:
p : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ p
hirr : Irreducible (M := K[X]) (cyclotomic p K)
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ HAdd.hAdd (α := ℕ) 0 1} K L
hζ' : IsPrimitiveRoot ζ (p ^ HAdd.hAdd (α := ℕ) 0 1)
h : HPow.hPow (α := K) (-1) ((p - 1) / 2) = HPow.hPow (α := K) (-1) (φ (p ^ HAdd.hAdd (α := ℕ) 0 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 - 1) / 2) * HPow.hPow (α := K) (↑p : K) (p - 2)
have h₁ : HPow.hPow (α := K) (↑p : K) (p - 2) =
  HPow.hPow (α := K) (↑p : K) (HPow.hPow (β := ℕ) p 0 * ((p - 1) * HAdd.hAdd (α := ℕ) 0 1 - 1))
Tactic: convert! discr_prime_pow_ne_two hζ' (by simpa [hirr]) (by simp [hodd]) using 2