awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) (↑n : R)
μ : R
hf : Function.Injective (α := R) (β := FractionRing R) (⇑(algebraMap R (FractionRing R)) : (a : R) → FractionRing R)
this : NeZero.{u_1} (R := FractionRing R) (↑n : FractionRing R)
⊢ IsRoot (cyclotomic n R) μ ↔ IsPrimitiveRoot μ n
have rw : IsRoot (R := FractionRing R) (map (algebraMap R (FractionRing R)) (cyclotomic n R) : (FractionRing R)[X])
    ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) μ : FractionRing R) ↔
  IsPrimitiveRoot μ n
Tactic: rw [← isRoot_map_iff hf, ← IsPrimitiveRoot.map_iff_of_injective hf, map_cyclotomic, ←
    isRoot_cyclotomic_iff']
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) (↑n : R)
μ : R
hf : Function.Injective (α := R) (β := FractionRing R) (⇑(algebraMap R (FractionRing R)) : (a : R) → FractionRing R)
this : NeZero.{u_1} (R := FractionRing R) (↑n : FractionRing R)
rw :
  IsRoot (R := FractionRing R) (map (algebraMap R (FractionRing R)) (cyclotomic n R) : (FractionRing R)[X])
      ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) μ : FractionRing R) ↔
    IsPrimitiveRoot μ n
⊢ IsRoot (cyclotomic n R) μ ↔ IsPrimitiveRoot μ n
have rw₁ : IsRoot (R := FractionRing R) (map (algebraMap R (FractionRing R)) (cyclotomic n R) : (FractionRing R)[X])
    ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) μ : FractionRing R) ↔
  IsPrimitiveRoot (M := FractionRing R) ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) μ : FractionRing R)
    n
Tactic: rw [← isRoot_map_iff hf, ← IsPrimitiveRoot.map_iff_of_injective hf, map_cyclotomic, ←
    isRoot_cyclotomic_iff']
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) (↑n : R)
μ : R
hf : Function.Injective (α := R) (β := FractionRing R) (⇑(algebraMap R (FractionRing R)) : (a : R) → FractionRing R)
this : NeZero.{u_1} (R := FractionRing R) (↑n : FractionRing R)
rw :
  IsRoot (R := FractionRing R) (map (algebraMap R (FractionRing R)) (cyclotomic n R) : (FractionRing R)[X])
      ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) μ : FractionRing R) ↔
    IsPrimitiveRoot μ n
rw₁ :
  IsRoot (R := FractionRing R) (map (algebraMap R (FractionRing R)) (cyclotomic n R) : (FractionRing R)[X])
      ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) μ : FractionRing R) ↔
    IsPrimitiveRoot (M := FractionRing R)
      ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) μ : FractionRing R) n
⊢ IsRoot (cyclotomic n R) μ ↔ IsPrimitiveRoot μ n
have rw₂ : IsRoot (R := FractionRing R) (cyclotomic n (FractionRing R) : (FractionRing R)[X])
    ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) μ : FractionRing R) ↔
  IsPrimitiveRoot (M := FractionRing R) ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) μ : FractionRing R)
    n
Tactic: rw [← isRoot_map_iff hf, ← IsPrimitiveRoot.map_iff_of_injective hf, map_cyclotomic, ←
    isRoot_cyclotomic_iff']
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) (↑n : R)
μ : R
hf : Function.Injective (α := R) (β := FractionRing R) (⇑(algebraMap R (FractionRing R)) : (a : R) → FractionRing R)
this : NeZero.{u_1} (R := FractionRing R) (↑n : FractionRing R)
rw :
  IsRoot (R := FractionRing R) (map (algebraMap R (FractionRing R)) (cyclotomic n R) : (FractionRing R)[X])
      ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) μ : FractionRing R) ↔
    IsPrimitiveRoot μ n
rw₁ :
  IsRoot (R := FractionRing R) (map (algebraMap R (FractionRing R)) (cyclotomic n R) : (FractionRing R)[X])
      ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) μ : FractionRing R) ↔
    IsPrimitiveRoot (M := FractionRing R)
      ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) μ : FractionRing R) n
rw₂ :
  IsRoot (R := FractionRing R) (cyclotomic n (FractionRing R) : (FractionRing R)[X])
      ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) μ : FractionRing R) ↔
    IsPrimitiveRoot (M := FractionRing R)
      ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) μ : FractionRing R) n
⊢ IsRoot (cyclotomic n R) μ ↔ IsPrimitiveRoot μ n
have rw₃ : IsRoot (R := FractionRing R) (cyclotomic n (FractionRing R) : (FractionRing R)[X])
    ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) μ : FractionRing R) ↔
  IsRoot (R := FractionRing R) (cyclotomic n (FractionRing R) : (FractionRing R)[X])
    ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) μ : FractionRing R)
Tactic: rw [← isRoot_map_iff hf, ← IsPrimitiveRoot.map_iff_of_injective hf, map_cyclotomic, ←
    isRoot_cyclotomic_iff']
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) (↑n : R)
⊢ (roots (cyclotomic n R)).Nodup
have inl : ∀ (h : roots (cyclotomic n R) = 0), (roots (cyclotomic n R)).Nodup
Tactic: obtain h | ⟨ζ, hζ⟩ := (cyclotomic n R).roots.empty_or_exists_mem
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) (↑n : R)
inl : ∀ (h : roots (cyclotomic n R) = 0), (roots (cyclotomic n R)).Nodup
⊢ (roots (cyclotomic n R)).Nodup
have inr : ∀ (ζ : R) (hζ : ζ ∈ roots (cyclotomic n R)), (roots (cyclotomic n R)).Nodup
Tactic: obtain h | ⟨ζ, hζ⟩ := (cyclotomic n R).roots.empty_or_exists_mem
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) (↑n : R)
ζ : R
hζ : ζ ∈ roots (cyclotomic n R)
⊢ (roots (cyclotomic n R)).Nodup
have hζ₁ : IsPrimitiveRoot ζ n
Tactic: rw [mem_roots <| cyclotomic_ne_zero n R, isRoot_cyclotomic_iff] at hζ
Cleared hypotheses: hζ
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) (↑n : R)
⊢ { val := roots (cyclotomic n R), nodup := ⋯ : Finset R } = primitiveRoots n R
have h : ∀ (a : R), a ∈ { val := roots (cyclotomic n R), nodup := sorry : Finset R } ↔ a ∈ primitiveRoots n R
Tactic: ext a
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) (↑n : R)
⊢ roots (cyclotomic n R) = (primitiveRoots n R).val
have rw : roots (cyclotomic n R) = { val := roots (cyclotomic n R), nodup := sorry }.val
Tactic: rw [← cyclotomic.roots_to_finset_eq_primitiveRoots]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
n m : ℕ
hnm : Eq (α := R[X]) (cyclotomic n R) (cyclotomic m R)
⊢ n = m
have inl : ∀ (hnm : Eq (α := R[X]) (cyclotomic 0 R) (cyclotomic m R)), 0 = m
Tactic: rcases eq_or_ne n 0 with (rfl | hzero)
Cleared hypotheses: n, hnm
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
n m : ℕ
hnm : Eq (α := R[X]) (cyclotomic n R) (cyclotomic m R)
inl : ∀ (hnm : Eq (α := R[X]) (cyclotomic 0 R) (cyclotomic m R)), 0 = m
⊢ n = m
have inr : ∀ (hzero : n ≠ 0), n = m
Tactic: rcases eq_or_ne n 0 with (rfl | hzero)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
m : ℕ
hnm : Eq (α := R[X]) (cyclotomic 0 R) (cyclotomic m R)
⊢ 0 = m
have hnm₁ : Eq (α := R[X]) 1 (cyclotomic m R)
Tactic: rw [cyclotomic_zero] at hnm
Cleared hypotheses: hnm
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
m : ℕ
hnm : Eq (α := R[X]) 1 (cyclotomic m R)
⊢ 0 = m
have hnm₁ : natDegree.{u_1} (R := R) 1 = natDegree (cyclotomic m R)
Tactic: replace hnm := congr_arg natDegree hnm
Cleared hypotheses: hnm
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
m : ℕ
hnm : natDegree.{u_1} (R := R) 1 = natDegree (cyclotomic m R)
⊢ 0 = m
have inl : ∀ (hnm : 0 = natDegree (cyclotomic m R)), 0 = m
Tactic: rwa [natDegree_one, natDegree_cyclotomic, eq_comm, Nat.totient_eq_zero, eq_comm] at hnm
Cleared hypotheses: hnm
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
m : ℕ
hnm : natDegree.{u_1} (R := R) 1 = natDegree (cyclotomic m R)
inl : ∀ (hnm : 0 = natDegree (cyclotomic m R)), 0 = m
⊢ 0 = m
have inl₁ : ∀ (hnm : 0 = m.totient), 0 = m
Tactic: rwa [natDegree_one, natDegree_cyclotomic, eq_comm, Nat.totient_eq_zero, eq_comm] at hnm
Cleared hypotheses: hnm
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
m : ℕ
hnm : natDegree.{u_1} (R := R) 1 = natDegree (cyclotomic m R)
inl : ∀ (hnm : 0 = natDegree (cyclotomic m R)), 0 = m
inl₁ : ∀ (hnm : 0 = m.totient), 0 = m
⊢ 0 = m
have inl₂ : ∀ (hnm : m.totient = 0), 0 = m
Tactic: rwa [natDegree_one, natDegree_cyclotomic, eq_comm, Nat.totient_eq_zero, eq_comm] at hnm
Cleared hypotheses: hnm
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
m : ℕ
hnm : natDegree.{u_1} (R := R) 1 = natDegree (cyclotomic m R)
inl : ∀ (hnm : 0 = natDegree (cyclotomic m R)), 0 = m
inl₁ : ∀ (hnm : 0 = m.totient), 0 = m
inl₂ : ∀ (hnm : m.totient = 0), 0 = m
⊢ 0 = m
have inl₃ : ∀ (hnm : m = 0), 0 = m
Tactic: rwa [natDegree_one, natDegree_cyclotomic, eq_comm, Nat.totient_eq_zero, eq_comm] at hnm
Cleared hypotheses: hnm
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
m : ℕ
hnm : natDegree.{u_1} (R := R) 1 = natDegree (cyclotomic m R)
inl : ∀ (hnm : 0 = natDegree (cyclotomic m R)), 0 = m
inl₁ : ∀ (hnm : 0 = m.totient), 0 = m
inl₂ : ∀ (hnm : m.totient = 0), 0 = m
inl₃ : ∀ (hnm : m = 0), 0 = m
⊢ 0 = m
have inl₄ : ∀ (hnm : 0 = m), 0 = m
Tactic: rwa [natDegree_one, natDegree_cyclotomic, eq_comm, Nat.totient_eq_zero, eq_comm] at hnm
Cleared hypotheses: hnm
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
n m : ℕ
hnm : Eq (α := R[X]) (cyclotomic n R) (cyclotomic m R)
hzero : n ≠ 0
⊢ n = m
have this : NeZero n
Tactic: haveI := NeZero.mk hzero
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
n m : ℕ
hnm : Eq (α := R[X]) (cyclotomic n R) (cyclotomic m R)
hzero : n ≠ 0
this : NeZero n
⊢ n = m
have hnm₁ : Eq.{u_1 + 1} (α := R[X]) (map (Int.castRingHom R) (cyclotomic n ℤ)) (map (Int.castRingHom R) (cyclotomic m ℤ))
Tactic: rw [← map_cyclotomic_int _ R, ← map_cyclotomic_int _ R] at hnm
Cleared hypotheses: hnm, hzero, this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
n m : ℕ
hnm : Eq.{u_1 + 1} (α := R[X]) (map (Int.castRingHom R) (cyclotomic n ℤ)) (map (Int.castRingHom R) (cyclotomic m ℤ))
hzero : n ≠ 0
this : NeZero n
⊢ n = m
have hnm₁ : cyclotomic n ℤ = cyclotomic m ℤ
Tactic: replace hnm := map_injective (Int.castRingHom R) Int.cast_injective hnm
Cleared hypotheses: hnm
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
n m : ℕ
hzero : n ≠ 0
this : NeZero n
hnm : cyclotomic n ℤ = cyclotomic m ℤ
⊢ n = m
have hnm₁ : map (Int.castRingHom ℂ) (cyclotomic n ℤ) = map (Int.castRingHom ℂ) (cyclotomic m ℤ)
Tactic: replace hnm := congr_arg (map (Int.castRingHom ℂ)) hnm
Cleared hypotheses: hnm
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
n m : ℕ
hzero : n ≠ 0
this : NeZero n
hnm : map (Int.castRingHom ℂ) (cyclotomic n ℤ) = map (Int.castRingHom ℂ) (cyclotomic m ℤ)
⊢ n = m
have hnm₁ : cyclotomic n ℂ = cyclotomic m ℂ
Tactic: rw [map_cyclotomic_int, map_cyclotomic_int] at hnm
Cleared hypotheses: hnm
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
n m : ℕ
hzero : n ≠ 0
this : NeZero n
hnm : cyclotomic n ℂ = cyclotomic m ℂ
⊢ n = m
have hprim : IsPrimitiveRoot (Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ))) n
Tactic: have hprim := Complex.isPrimitiveRoot_exp _ hzero
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
n m : ℕ
hzero : n ≠ 0
this : NeZero n
hnm : cyclotomic n ℂ = cyclotomic m ℂ
hprim : IsPrimitiveRoot (Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ))) n
⊢ n = m
have hroot : IsRoot (cyclotomic n ℂ) (Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ)))
Tactic: have hroot := isRoot_cyclotomic_iff (R := ℂ).2 hprim
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
n m : ℕ
hzero : n ≠ 0
this : NeZero n
hnm : cyclotomic n ℂ = cyclotomic m ℂ
hprim : IsPrimitiveRoot (Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ))) n
hroot : IsRoot (cyclotomic n ℂ) (Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ)))
⊢ n = m
have hroot₁ : IsRoot (cyclotomic m ℂ) (Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ)))
Tactic: rw [hnm] at hroot
Cleared hypotheses: hroot
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
n m : ℕ
hzero : n ≠ 0
this : NeZero n
hnm : cyclotomic n ℂ = cyclotomic m ℂ
hprim : IsPrimitiveRoot (Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ))) n
hroot : IsRoot (cyclotomic m ℂ) (Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ)))
⊢ n = m
have hmzero : NeZero m
Tactic: haveI hmzero : NeZero m := ⟨fun h => by simp [h] at hroot⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
n m : ℕ
hzero : n ≠ 0
this : NeZero n
hnm : cyclotomic n ℂ = cyclotomic m ℂ
hprim : IsPrimitiveRoot (Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ))) n
hroot : IsRoot (cyclotomic m ℂ) (Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ)))
hmzero : NeZero m
⊢ n = m
have hroot₁ : IsPrimitiveRoot (Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ))) m
Tactic: rw [isRoot_cyclotomic_iff (R := ℂ)] at hroot
Cleared hypotheses: hroot, hmzero
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
n m : ℕ
hzero : n ≠ 0
this : NeZero n
hnm : cyclotomic n ℂ = cyclotomic m ℂ
hprim : IsPrimitiveRoot (Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ))) n
hroot : IsPrimitiveRoot (Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ))) m
hmzero : NeZero m
⊢ n = m
have hprim₁ : n = orderOf (Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ)))
Tactic: replace hprim := hprim.eq_orderOf
Cleared hypotheses: hprim
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
n m : ℕ
hzero : n ≠ 0
this : NeZero n
hnm : cyclotomic n ℂ = cyclotomic m ℂ
hroot : IsPrimitiveRoot (Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ))) m
hmzero : NeZero m
hprim : n = orderOf (Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ)))
⊢ n = m
have inr : ∀ (hprim : n = m), n = m
Tactic: rwa [← IsPrimitiveRoot.eq_orderOf hroot] at hprim
Cleared hypotheses: hprim
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
n : ℕ
K : Type u_2
inst : Field K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
inst_1 : CharZero K
⊢ minpoly ℤ μ ∣ cyclotomic n ℤ
have apply : Eq (α := K) ((aeval μ : (a : ℤ[X]) → K) (cyclotomic n ℤ) : K) (0 : K)
Tactic: apply minpoly.isIntegrallyClosed_dvd (h.isIntegral hpos)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (hypothesis)
Goal:
K : Type u_2
inst : Field K
R : Type u_3
inst_1 : CommRing R
inst_2 : IsDomain R
μ : R
n : ℕ
inst_3 : Algebra K R
hμ : IsPrimitiveRoot μ n
h : Irreducible (M := K[X]) (cyclotomic n K)
inst_4 : NeZero.{u_2} (R := K) (↑n : K)
⊢ Eq (α := K[X]) (cyclotomic n K) (minpoly K μ)
have this : NeZero.{u_3} (R := R) (↑n : R)
Tactic: haveI := NeZero.of_faithfulSMul K R n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
K : Type u_2
inst : Field K
R : Type u_3
inst_1 : CommRing R
inst_2 : IsDomain R
μ : R
n : ℕ
inst_3 : Algebra K R
hμ : IsPrimitiveRoot μ n
h : Irreducible (M := K[X]) (cyclotomic n K)
inst_4 : NeZero.{u_2} (R := K) (↑n : K)
this : NeZero.{u_3} (R := R) (↑n : R)
⊢ Eq (α := K[X]) (cyclotomic n K) (minpoly K μ)
have refine : Eq.{u_3 + 1} (α := R) ((aeval μ : (a : K[X]) → R) (cyclotomic n K) : R) (0 : R)
Tactic: refine minpoly.eq_of_irreducible_of_monic h ?_ (cyclotomic.monic n K)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
K : Type u_2
inst : Field K
R : Type u_3
inst_1 : CommRing R
inst_2 : IsDomain R
μ : R
n : ℕ
inst_3 : Algebra K R
hμ : IsPrimitiveRoot μ n
h : Irreducible (M := K[X]) (cyclotomic n K)
inst_4 : NeZero.{u_2} (R := K) (↑n : K)
this : NeZero.{u_3} (R := R) (↑n : R)
⊢ Eq.{u_3 + 1} (α := R) ((aeval μ : (a : K[X]) → R) (cyclotomic n K) : R) (0 : R)
have rwa : eval₂ (algebraMap K R) μ (cyclotomic n K) = 0
Tactic: rwa [aeval_def, eval₂_eq_eval_map, map_cyclotomic, ← IsRoot.def, isRoot_cyclotomic_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
K : Type u_2
inst : Field K
R : Type u_3
inst_1 : CommRing R
inst_2 : IsDomain R
μ : R
n : ℕ
inst_3 : Algebra K R
hμ : IsPrimitiveRoot μ n
h : Irreducible (M := K[X]) (cyclotomic n K)
inst_4 : NeZero.{u_2} (R := K) (↑n : K)
this : NeZero.{u_3} (R := R) (↑n : R)
rwa : eval₂ (algebraMap K R) μ (cyclotomic n K) = 0
⊢ Eq.{u_3 + 1} (α := R) ((aeval μ : (a : K[X]) → R) (cyclotomic n K) : R) (0 : R)
have rwa₁ : eval μ (map (algebraMap K R) (cyclotomic n K)) = 0
Tactic: rwa [aeval_def, eval₂_eq_eval_map, map_cyclotomic, ← IsRoot.def, isRoot_cyclotomic_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
K : Type u_2
inst : Field K
R : Type u_3
inst_1 : CommRing R
inst_2 : IsDomain R
μ : R
n : ℕ
inst_3 : Algebra K R
hμ : IsPrimitiveRoot μ n
h : Irreducible (M := K[X]) (cyclotomic n K)
inst_4 : NeZero.{u_2} (R := K) (↑n : K)
this : NeZero.{u_3} (R := R) (↑n : R)
rwa : eval₂ (algebraMap K R) μ (cyclotomic n K) = 0
rwa₁ : eval μ (map (algebraMap K R) (cyclotomic n K)) = 0
⊢ Eq.{u_3 + 1} (α := R) ((aeval μ : (a : K[X]) → R) (cyclotomic n K) : R) (0 : R)
have rwa₂ : eval μ (cyclotomic n R) = 0
Tactic: rwa [aeval_def, eval₂_eq_eval_map, map_cyclotomic, ← IsRoot.def, isRoot_cyclotomic_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
K : Type u_2
inst : Field K
R : Type u_3
inst_1 : CommRing R
inst_2 : IsDomain R
μ : R
n : ℕ
inst_3 : Algebra K R
hμ : IsPrimitiveRoot μ n
h : Irreducible (M := K[X]) (cyclotomic n K)
inst_4 : NeZero.{u_2} (R := K) (↑n : K)
this : NeZero.{u_3} (R := R) (↑n : R)
rwa : eval₂ (algebraMap K R) μ (cyclotomic n K) = 0
rwa₁ : eval μ (map (algebraMap K R) (cyclotomic n K)) = 0
rwa₂ : eval μ (cyclotomic n R) = 0
⊢ Eq.{u_3 + 1} (α := R) ((aeval μ : (a : K[X]) → R) (cyclotomic n K) : R) (0 : R)
have rwa₃ : IsRoot (cyclotomic n R) μ
Tactic: rwa [aeval_def, eval₂_eq_eval_map, map_cyclotomic, ← IsRoot.def, isRoot_cyclotomic_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
n : ℕ
K : Type u_2
inst : Field K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
inst_1 : CharZero K
⊢ cyclotomic n ℤ = minpoly ℤ μ
have refine : natDegree (cyclotomic n ℤ) ≤ natDegree (minpoly ℤ μ)
Tactic: refine eq_of_monic_of_dvd_of_natDegree_le (minpoly.monic (IsPrimitiveRoot.isIntegral h hpos))
    (cyclotomic.monic n ℤ) (h.minpoly_dvd_cyclotomic hpos) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
n : ℕ
K : Type u_2
inst : Field K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
inst_1 : CharZero K
⊢ cyclotomic n ℚ = minpoly ℚ μ
have rw : map (Int.castRingHom ℚ) (minpoly ℤ μ) = minpoly ℚ μ
Tactic: rw [← map_cyclotomic_int, cyclotomic_eq_minpoly h hpos]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
n : ℕ
hpos : 0 < n
⊢ Irreducible (M := ℤ[X]) (cyclotomic n ℤ)
have rw : Irreducible (M := ℤ[X]) (minpoly ℤ (cexp (2 * (↑Real.pi : ℂ) * I / (↑n : ℂ))))
Tactic: rw [cyclotomic_eq_minpoly (isPrimitiveRoot_exp n hpos.ne') hpos]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
n : ℕ
hpos : 0 < n
⊢ Irreducible (M := ℤ[X]) (minpoly ℤ (cexp (2 * (↑Real.pi : ℂ) * I / (↑n : ℂ))))
have hx : IsIntegral ℤ (cexp (2 * (↑Real.pi : ℂ) * I / (↑n : ℂ)))
Tactic: apply minpoly.irreducible
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
n : ℕ
hpos : 0 < n
⊢ Irreducible (M := ℚ[X]) (cyclotomic n ℚ)
have rw : Irreducible (map (Int.castRingHom ℚ) (cyclotomic n ℤ))
Tactic: rw [← map_cyclotomic_int]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
n m : ℕ
h : n ≠ m
⊢ IsCoprime (cyclotomic n ℚ) (cyclotomic m ℚ)
have inl : ∀ (h : 0 ≠ m), IsCoprime (cyclotomic 0 ℚ) (cyclotomic m ℚ)
Tactic: rcases n.eq_zero_or_pos with (rfl | hnzero)
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
n m : ℕ
h : n ≠ m
inl : ∀ (h : 0 ≠ m), IsCoprime (cyclotomic 0 ℚ) (cyclotomic m ℚ)
⊢ IsCoprime (cyclotomic n ℚ) (cyclotomic m ℚ)
have inr : ∀ (hnzero : n > 0), IsCoprime (cyclotomic n ℚ) (cyclotomic m ℚ)
Tactic: rcases n.eq_zero_or_pos with (rfl | hnzero)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
n m : ℕ
h : n ≠ m
hnzero : n > 0
⊢ IsCoprime (cyclotomic n ℚ) (cyclotomic m ℚ)
have inr : ∀ (h : n ≠ 0), IsCoprime (cyclotomic n ℚ) (cyclotomic 0 ℚ)
Tactic: rcases m.eq_zero_or_pos with (rfl | hmzero)
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
n m : ℕ
h : n ≠ m
hnzero : n > 0
inr : ∀ (h : n ≠ 0), IsCoprime (cyclotomic n ℚ) (cyclotomic 0 ℚ)
⊢ IsCoprime (cyclotomic n ℚ) (cyclotomic m ℚ)
have inr₁ : ∀ (hmzero : m > 0), IsCoprime (cyclotomic n ℚ) (cyclotomic m ℚ)
Tactic: rcases m.eq_zero_or_pos with (rfl | hmzero)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
n m : ℕ
h : n ≠ m
hnzero : n > 0
hmzero : m > 0
⊢ IsCoprime (cyclotomic n ℚ) (cyclotomic m ℚ)
have inr : ¬cyclotomic n ℚ ∣ cyclotomic m ℚ
Tactic: rw [Irreducible.coprime_iff_not_dvd <| cyclotomic.irreducible_rat <| hnzero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
⊢ Eq.{u_1 + 1} (α := K) (∑ i : Fin p, (↑(α i) : K) * ζ ^ (↑i : ℕ)) 0 ↔ ∀ (i j : Fin p), α i = α j
have this : Fact (Nat.Prime p)
Tactic: haveI : Fact p.Prime := ⟨hp⟩