awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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)
⊢ NeZero.{u_1} (R := FractionRing R) (↑n : FractionRing R)

Tactic:
haveI : NeZero (n : FractionRing R) := NeZero.nat_of_injective hf
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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
rw₃ 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)
⊢ IsRoot (cyclotomic n R) μ ↔ IsPrimitiveRoot μ n

Tactic:
rw [← isRoot_map_iff hf, ← IsPrimitiveRoot.map_iff_of_injective hf, map_cyclotomic, ←
    isRoot_cyclotomic_iff']

Premises used: _private.0.Polynomial.isRoot_cyclotomic_iff', IsPrimitiveRoot.map_iff_of_injective, Polynomial.map_cyclotomic, Polynomial.isRoot_map_iff
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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
inr : ∀ (ζ : R) (hζ : ζ ∈ roots (cyclotomic n R)), (roots (cyclotomic n R)).Nodup
⊢ (roots (cyclotomic n R)).Nodup

Tactic:
obtain h | ⟨ζ, hζ⟩ := (cyclotomic n R).roots.empty_or_exists_mem

Premises used: Polynomial.roots, Polynomial.cyclotomic, Multiset.empty_or_exists_mem
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) (↑n : R)
h : roots (cyclotomic n R) = 0
⊢ (roots (cyclotomic n R)).Nodup

Tactic:
h.symm ▸ Multiset.nodup_zero

Premises used: Eq.rec, Eq.symm, Multiset.nodup_zero
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) (↑n : R)
h : roots (cyclotomic n R) = 0
⊢ (roots (cyclotomic n R)).Nodup

Tactic:
exact h.symm ▸ Multiset.nodup_zero
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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)
⊢ IsPrimitiveRoot ζ n

Tactic:
rw [mem_roots <| cyclotomic_ne_zero n R, isRoot_cyclotomic_iff] at hζ

Premises used: Polynomial.cyclotomic_ne_zero, Polynomial.mem_roots, Polynomial.isRoot_cyclotomic_iff
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) (↑n : R)
ζ : R
hζ : IsPrimitiveRoot ζ n
⊢ (roots (cyclotomic n R)).Nodup

Tactic:
Multiset.nodup_of_le
    (roots.le_of_dvd (X_pow_sub_C_ne_zero (NeZero.pos_of_neZero_natCast R) 1) <|
      cyclotomic.dvd_X_pow_sub_one n R) hζ.nthRoots_one_nodup

Premises used: Multiset.nodup_of_le, NeZero.pos_of_neZero_natCast, Polynomial.cyclotomic.dvd_X_pow_sub_one, IsPrimitiveRoot.nthRoots_one_nodup, Polynomial.roots.le_of_dvd, OfNat.ofNat, Polynomial.X_pow_sub_C_ne_zero
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) (↑n : R)
ζ : R
hζ : IsPrimitiveRoot ζ n
⊢ (roots (cyclotomic n R)).Nodup

Tactic:
refine Multiset.nodup_of_le
    (roots.le_of_dvd (X_pow_sub_C_ne_zero (NeZero.pos_of_neZero_natCast R) 1) <|
      cyclotomic.dvd_X_pow_sub_one n R) hζ.nthRoots_one_nodup

Premises used: Multiset.nodup_of_le, NeZero.pos_of_neZero_natCast, Polynomial.cyclotomic.dvd_X_pow_sub_one, IsPrimitiveRoot.nthRoots_one_nodup, Polynomial.roots.le_of_dvd, OfNat.ofNat, Polynomial.X_pow_sub_C_ne_zero
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) (↑n : R)
h : ∀ (a : R), a ∈ { val := roots (cyclotomic n R), nodup := ⋯ : Finset R } ↔ a ∈ primitiveRoots n R
⊢ { val := roots (cyclotomic n R), nodup := ⋯ : Finset R } = primitiveRoots n R

Tactic:
ext a
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) (↑n : R)
a : R
⊢ a ∈ { val := roots (cyclotomic n R), nodup := ⋯ : Finset R } ↔ a ∈ primitiveRoots n R

Tactic:
simp [cyclotomic_ne_zero n R, ← isRoot_cyclotomic_iff, mem_primitiveRoots,
    NeZero.pos_of_neZero_natCast R]

Premises used: Polynomial.cyclotomic_ne_zero, NeZero.pos_of_neZero_natCast, mem_primitiveRoots, Polynomial.isRoot_cyclotomic_iff
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) (↑n : R)
rw rw₁ : roots (cyclotomic n R) = { val := roots (cyclotomic n R), nodup := ⋯ }.val
⊢ roots (cyclotomic n R) = (primitiveRoots n R).val

Tactic:
rw [← cyclotomic.roots_to_finset_eq_primitiveRoots]

Premises used: Polynomial.cyclotomic.roots_to_finset_eq_primitiveRoots
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
n : ℕ
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CharZero R
μ : R
hn : 0 < n
⊢ IsRoot (cyclotomic n R) μ ↔ IsPrimitiveRoot μ n

Tactic:
letI := NeZero.of_gt hn
  isRoot_cyclotomic_iff

Premises used: Polynomial.isRoot_cyclotomic_iff
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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
inr : ∀ (hzero : n ≠ 0), n = m
⊢ n = m

Tactic:
rcases eq_or_ne n 0 with (rfl | hzero)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
m : ℕ
hnm : Eq (α := R[X]) (cyclotomic 0 R) (cyclotomic m R)
⊢ Eq (α := R[X]) 1 (cyclotomic m R)

Tactic:
rw [cyclotomic_zero] at hnm

Premises used: Polynomial.cyclotomic_zero
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
m : ℕ
hnm : Eq (α := R[X]) 1 (cyclotomic m R)
⊢ natDegree.{u_1} (R := R) 1 = natDegree (cyclotomic m R)

Tactic:
replace hnm := congr_arg natDegree hnm
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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
inl₄ inl₅ inl₆ inl₇ : ∀ (hnm : 0 = m), 0 = m
⊢ 0 = m

Tactic:
rwa [natDegree_one, natDegree_cyclotomic, eq_comm, Nat.totient_eq_zero, eq_comm] at hnm

Premises used: Polynomial.natDegree_cyclotomic, eq_comm, Nat.totient_eq_zero, Polynomial.natDegree_one
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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
⊢ NeZero n

Tactic:
haveI := NeZero.mk hzero
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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
⊢ 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

Premises used: Polynomial.map_cyclotomic_int
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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
hnm₁ : Eq.{u_1 + 1} (α := R[X]) (map (Int.castRingHom R) (cyclotomic n ℤ)) (map (Int.castRingHom R) (cyclotomic m ℤ))
⊢ n ≠ 0

Tactic:
rw [← map_cyclotomic_int _ R, ← map_cyclotomic_int _ R] at hnm

Premises used: Polynomial.map_cyclotomic_int
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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
hnm₁ : Eq.{u_1 + 1} (α := R[X]) (map (Int.castRingHom R) (cyclotomic n ℤ)) (map (Int.castRingHom R) (cyclotomic m ℤ))
hzero₁ : n ≠ 0
⊢ NeZero n

Tactic:
rw [← map_cyclotomic_int _ R, ← map_cyclotomic_int _ R] at hnm

Premises used: Polynomial.map_cyclotomic_int
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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
⊢ cyclotomic n ℤ = cyclotomic m ℤ

Tactic:
replace hnm := map_injective (Int.castRingHom R) Int.cast_injective hnm
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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 ℤ
⊢ map (Int.castRingHom ℂ) (cyclotomic n ℤ) = map (Int.castRingHom ℂ) (cyclotomic m ℤ)

Tactic:
replace hnm := congr_arg (map (Int.castRingHom ℂ)) hnm
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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 ℤ)
⊢ cyclotomic n ℂ = cyclotomic m ℂ

Tactic:
rw [map_cyclotomic_int, map_cyclotomic_int] at hnm

Premises used: Polynomial.map_cyclotomic_int
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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 ℂ
⊢ IsPrimitiveRoot (Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ))) n

Tactic:
have hprim := Complex.isPrimitiveRoot_exp _ hzero
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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
⊢ IsRoot (cyclotomic n ℂ) (Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ)))

Tactic:
have hroot := isRoot_cyclotomic_iff (R := ℂ).2 hprim
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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 : ℂ)))
⊢ IsRoot (cyclotomic m ℂ) (Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ)))

Tactic:
rw [hnm] at hroot
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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 : ℂ)))
h : m = 0
⊢ False

Tactic:
simp [h] at hroot
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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 : ℂ)))
⊢ NeZero m

Tactic:
haveI hmzero : NeZero m := ⟨fun h => by simp [h] at hroot⟩
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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
⊢ IsPrimitiveRoot (Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ))) m

Tactic:
rw [isRoot_cyclotomic_iff (R := ℂ)] at hroot

Premises used: Polynomial.isRoot_cyclotomic_iff
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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
hroot₁ : IsPrimitiveRoot (Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ))) m
⊢ NeZero m

Tactic:
rw [isRoot_cyclotomic_iff (R := ℂ)] at hroot

Premises used: Polynomial.isRoot_cyclotomic_iff
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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 = orderOf (Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ)))

Tactic:
replace hprim := hprim.eq_orderOf
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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 : ℂ)))
inr inr₁ inr₂ inr₃ : ∀ (hprim : n = m), n = m
⊢ n = m

Tactic:
rwa [← IsPrimitiveRoot.eq_orderOf hroot] at hprim

Premises used: IsPrimitiveRoot.eq_orderOf
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
n : ℕ
K : Type u_2
inst : Field K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
inst_1 : CharZero K
apply : Eq (α := K) ((aeval μ : (a : ℤ[X]) → K) (cyclotomic n ℤ) : K) (0 : K)
⊢ minpoly ℤ μ ∣ cyclotomic n ℤ

Tactic:
apply minpoly.isIntegrallyClosed_dvd (h.isIntegral hpos)

Premises used: IsPrimitiveRoot.isIntegral, minpoly.isIntegrallyClosed_dvd
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
n : ℕ
K : Type u_2
inst : Field K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
inst_1 : CharZero K
⊢ Eq (α := K) ((aeval μ : (a : ℤ[X]) → K) (cyclotomic n ℤ) : K) (0 : K)

Tactic:
simpa [aeval_def, eval₂_eq_eval_map, IsRoot.def] using h.isRoot_cyclotomic hpos

Premises used: Polynomial.IsRoot.def, Polynomial.aeval_def, Polynomial.eval₂_eq_eval_map, IsPrimitiveRoot.isRoot_cyclotomic
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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)
⊢ NeZero.{u_3} (R := R) (↑n : R)

Tactic:
haveI := NeZero.of_faithfulSMul K R n
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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 μ)

Tactic:
minpoly.eq_of_irreducible_of_monic h ?_ (cyclotomic.monic n K)

Premises used: minpoly.eq_of_irreducible_of_monic, Polynomial.cyclotomic.monic
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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)
refine : Eq.{u_3 + 1} (α := R) ((aeval μ : (a : K[X]) → R) (cyclotomic n K) : R) (0 : R)
⊢ Eq (α := K[X]) (cyclotomic n K) (minpoly K μ)

Tactic:
refine minpoly.eq_of_irreducible_of_monic h ?_ (cyclotomic.monic n K)

Premises used: minpoly.eq_of_irreducible_of_monic, Polynomial.cyclotomic.monic
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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
rwa₃ : IsRoot (cyclotomic n R) μ
rwa₄ rwa₅ rwa₆ rwa₇ : IsPrimitiveRoot μ n
⊢ Eq.{u_3 + 1} (α := R) ((aeval μ : (a : K[X]) → R) (cyclotomic n K) : R) (0 : R)

Tactic:
rwa [aeval_def, eval₂_eq_eval_map, map_cyclotomic, ← IsRoot.def, isRoot_cyclotomic_iff]

Premises used: Polynomial.IsRoot.def, Polynomial.aeval_def, Polynomial.map_cyclotomic, Polynomial.eval₂_eq_eval_map, Polynomial.isRoot_cyclotomic_iff
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
n : ℕ
K : Type u_2
inst : Field K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
inst_1 : CharZero K
⊢ cyclotomic n ℤ = minpoly ℤ μ

Tactic:
eq_of_monic_of_dvd_of_natDegree_le (minpoly.monic (IsPrimitiveRoot.isIntegral h hpos))
    (cyclotomic.monic n ℤ) (h.minpoly_dvd_cyclotomic hpos) ?_

Premises used: minpoly.monic, Int, IsPrimitiveRoot.isIntegral, Polynomial.eq_of_monic_of_dvd_of_natDegree_le, Polynomial.cyclotomic.monic, IsPrimitiveRoot.minpoly_dvd_cyclotomic
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
n : ℕ
K : Type u_2
inst : Field K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
inst_1 : CharZero K
refine : natDegree (cyclotomic n ℤ) ≤ natDegree (minpoly ℤ μ)
⊢ cyclotomic n ℤ = 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) ?_

Premises used: minpoly.monic, Int, IsPrimitiveRoot.isIntegral, Polynomial.eq_of_monic_of_dvd_of_natDegree_le, Polynomial.cyclotomic.monic, IsPrimitiveRoot.minpoly_dvd_cyclotomic
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
n : ℕ
K : Type u_2
inst : Field K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
inst_1 : CharZero K
⊢ natDegree (cyclotomic n ℤ) ≤ natDegree (minpoly ℤ μ)

Tactic:
simpa [natDegree_cyclotomic n ℤ] using totient_le_degree_minpoly h

Premises used: IsPrimitiveRoot.totient_le_degree_minpoly, Polynomial.natDegree_cyclotomic, Int
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
n : ℕ
K : Type u_2
inst : Field K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
inst_1 : CharZero K
rw : map (Int.castRingHom ℚ) (minpoly ℤ μ) = minpoly ℚ μ
⊢ cyclotomic n ℚ = minpoly ℚ μ

Tactic:
rw [← map_cyclotomic_int, cyclotomic_eq_minpoly h hpos]

Premises used: Polynomial.map_cyclotomic_int, Polynomial.cyclotomic_eq_minpoly
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
n : ℕ
K : Type u_2
inst : Field K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
inst_1 : CharZero K
⊢ map (Int.castRingHom ℚ) (minpoly ℤ μ) = minpoly ℚ μ

Tactic:
(minpoly.isIntegrallyClosed_eq_field_fractions' _ (IsPrimitiveRoot.isIntegral h hpos)).symm

Premises used: IsPrimitiveRoot.isIntegral, Eq.symm, minpoly.isIntegrallyClosed_eq_field_fractions'
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
n : ℕ
K : Type u_2
inst : Field K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
inst_1 : CharZero K
⊢ map (Int.castRingHom ℚ) (minpoly ℤ μ) = minpoly ℚ μ

Tactic:
exact (minpoly.isIntegrallyClosed_eq_field_fractions' _ (IsPrimitiveRoot.isIntegral h hpos)).symm

Premises used: IsPrimitiveRoot.isIntegral, Eq.symm, minpoly.isIntegrallyClosed_eq_field_fractions'
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
n : ℕ
hpos : 0 < n
rw : Irreducible (M := ℤ[X]) (minpoly ℤ (cexp (2 * (↑Real.pi : ℂ) * I / (↑n : ℂ))))
⊢ Irreducible (M := ℤ[X]) (cyclotomic n ℤ)

Tactic:
rw [cyclotomic_eq_minpoly (isPrimitiveRoot_exp n hpos.ne') hpos]

Premises used: Complex.isPrimitiveRoot_exp, LT.lt.ne', Polynomial.cyclotomic_eq_minpoly
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
n : ℕ
hpos : 0 < n
hx : IsIntegral ℤ (cexp (2 * (↑Real.pi : ℂ) * I / (↑n : ℂ)))
⊢ Irreducible (M := ℤ[X]) (minpoly ℤ (cexp (2 * (↑Real.pi : ℂ) * I / (↑n : ℂ))))

Tactic:
apply minpoly.irreducible

Premises used: minpoly.irreducible
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
n : ℕ
hpos : 0 < n
⊢ IsIntegral ℤ (cexp (2 * (↑Real.pi : ℂ) * I / (↑n : ℂ)))

Tactic:
(isPrimitiveRoot_exp n hpos.ne').isIntegral hpos

Premises used: IsPrimitiveRoot.isIntegral, Complex.isPrimitiveRoot_exp, LT.lt.ne'
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
n : ℕ
hpos : 0 < n
⊢ IsIntegral ℤ (cexp (2 * (↑Real.pi : ℂ) * I / (↑n : ℂ)))

Tactic:
exact (isPrimitiveRoot_exp n hpos.ne').isIntegral hpos

Premises used: IsPrimitiveRoot.isIntegral, Complex.isPrimitiveRoot_exp, LT.lt.ne'
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
n : ℕ
hpos : 0 < n
rw : Irreducible (map (Int.castRingHom ℚ) (cyclotomic n ℤ))
⊢ Irreducible (M := ℚ[X]) (cyclotomic n ℚ)

Tactic:
rw [← map_cyclotomic_int]

Premises used: Polynomial.map_cyclotomic_int
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
n : ℕ
hpos : 0 < n
⊢ Irreducible (map (Int.castRingHom ℚ) (cyclotomic n ℤ))

Tactic:
(IsPrimitive.irreducible_iff_irreducible_map_fraction_map (cyclotomic.isPrimitive n ℤ)).1
    (cyclotomic.irreducible hpos)

Premises used: Polynomial.cyclotomic.irreducible, Polynomial.IsPrimitive.irreducible_iff_irreducible_map_fraction_map, Int, Polynomial.cyclotomic.isPrimitive, Iff.mp
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
n : ℕ
hpos : 0 < n
⊢ Irreducible (map (Int.castRingHom ℚ) (cyclotomic n ℤ))

Tactic:
exact (IsPrimitive.irreducible_iff_irreducible_map_fraction_map (cyclotomic.isPrimitive n ℤ)).1
    (cyclotomic.irreducible hpos)

Premises used: Polynomial.cyclotomic.irreducible, Polynomial.IsPrimitive.irreducible_iff_irreducible_map_fraction_map, Int, Polynomial.cyclotomic.isPrimitive, Iff.mp
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
n m : ℕ
h : n ≠ m
inl : ∀ (h : 0 ≠ m), IsCoprime (cyclotomic 0 ℚ) (cyclotomic m ℚ)
inr : ∀ (hnzero : n > 0), IsCoprime (cyclotomic n ℚ) (cyclotomic m ℚ)
⊢ IsCoprime (cyclotomic n ℚ) (cyclotomic m ℚ)

Tactic:
rcases n.eq_zero_or_pos with (rfl | hnzero)

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
m : ℕ
h : 0 ≠ m
⊢ IsCoprime (cyclotomic 0 ℚ) (cyclotomic m ℚ)

Tactic:
isCoprime_one_left

Premises used: Polynomial.cyclotomic, dite, isCoprime_one_left
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
m : ℕ
h : 0 ≠ m
⊢ IsCoprime (cyclotomic 0 ℚ) (cyclotomic m ℚ)

Tactic:
exact isCoprime_one_left

Premises used: isCoprime_one_left