awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
inst_2 : CharZero K
ζ : K
n : ℕ+
h : IsPrimitiveRoot ζ (↑n : ℕ)
P : ℤ[X]
hP :
  Eq (α := K[X]) (map (Int.castRingHom K) P) (cyclotomic' (↑n : ℕ) K) ∧
    P.degree = degree (cyclotomic' (↑n : ℕ) K) ∧ P.Monic
⊢ ∃! P : ℤ[X], Eq (α := K[X]) (map (Int.castRingHom K) P) (cyclotomic' (↑n : ℕ) K)

Tactic:
⟨P, hP.1, fun Q hQ => ?_⟩

Premises used: And.left, ExistsUnique, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
inst_2 : CharZero K
ζ : K
n : ℕ+
h : IsPrimitiveRoot ζ (↑n : ℕ)
P : ℤ[X]
hP :
  Eq (α := K[X]) (map (Int.castRingHom K) P) (cyclotomic' (↑n : ℕ) K) ∧
    P.degree = degree (cyclotomic' (↑n : ℕ) K) ∧ P.Monic
refine :
  ∀ (Q : ℤ[X]) (hQ : (fun (P : ℤ[X]) ↦ Eq (α := K[X]) (map (Int.castRingHom K) P) (cyclotomic' (↑n : ℕ) K)) Q), Q = P
⊢ ∃! P : ℤ[X], Eq (α := K[X]) (map (Int.castRingHom K) P) (cyclotomic' (↑n : ℕ) K)

Tactic:
refine ⟨P, hP.1, fun Q hQ => ?_⟩
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
inst_2 : CharZero K
ζ : K
n : ℕ+
h : IsPrimitiveRoot ζ (↑n : ℕ)
P : ℤ[X]
hP :
  Eq (α := K[X]) (map (Int.castRingHom K) P) (cyclotomic' (↑n : ℕ) K) ∧
    P.degree = degree (cyclotomic' (↑n : ℕ) K) ∧ P.Monic
Q : ℤ[X]
hQ : (fun (P : ℤ[X]) ↦ Eq (α := K[X]) (map (Int.castRingHom K) P) (cyclotomic' (↑n : ℕ) K)) Q
a : Eq.{u_2 + 1} (α := K[X]) (map (Int.castRingHom K) Q) (map (Int.castRingHom K) P)
⊢ Q = P

Tactic:
apply map_injective (Int.castRingHom K) Int.cast_injective

Premises used: Polynomial.map_injective, Int.castRingHom, Int.cast_injective
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
inst_2 : CharZero K
ζ : K
n : ℕ+
h : IsPrimitiveRoot ζ (↑n : ℕ)
P : ℤ[X]
hP :
  Eq (α := K[X]) (map (Int.castRingHom K) P) (cyclotomic' (↑n : ℕ) K) ∧
    P.degree = degree (cyclotomic' (↑n : ℕ) K) ∧ P.Monic
Q : ℤ[X]
hQ : (fun (P : ℤ[X]) ↦ Eq (α := K[X]) (map (Int.castRingHom K) P) (cyclotomic' (↑n : ℕ) K)) Q
a : Eq (α := K[X]) (map (Int.castRingHom K) Q) (cyclotomic' (↑n : ℕ) K)
a₁ a₂ : Eq (α := K[X]) (cyclotomic' (↑n : ℕ) K) (cyclotomic' (↑n : ℕ) K)
⊢ Eq.{u_2 + 1} (α := K[X]) (map (Int.castRingHom K) Q) (map (Int.castRingHom K) P)

Tactic:
rw [hP.1, hQ]

Premises used: And.left
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
h : n ≠ 0
simp :
  map (Int.castRingHom ℤ)
      (⋯.choose (p := fun (P : ℤ[X]) ↦
        map (Int.castRingHom ℂ) P = cyclotomic' n ℂ ∧ P.degree = degree (cyclotomic' n ℂ) ∧ P.Monic)) =
    Exists.choose (p := fun (P : ℤ[X]) ↦
      map (Int.castRingHom ℂ) P = cyclotomic' n ℂ ∧ P.degree = degree (cyclotomic' n ℂ) ∧ P.Monic) ⋯
⊢ cyclotomic n ℤ =
    Exists.choose (p := fun (P : ℤ[X]) ↦
      map (Int.castRingHom ℂ) P = cyclotomic' n ℂ ∧ P.degree = degree (cyclotomic' n ℂ) ∧ P.Monic) ⋯

Tactic:
simp only [cyclotomic, h, dif_neg, not_false_iff]

Premises used: Polynomial.cyclotomic, dif_neg, not_false_iff
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
h : n ≠ 0
a :
  ∀ (i : ℕ),
    (map (Int.castRingHom ℤ)
            (⋯.choose (p := fun (P : ℤ[X]) ↦
              map (Int.castRingHom ℂ) P = cyclotomic' n ℂ ∧ P.degree = degree (cyclotomic' n ℂ) ∧ P.Monic))).coeff
        i =
      (Exists.choose (p := fun (P : ℤ[X]) ↦
            map (Int.castRingHom ℂ) P = cyclotomic' n ℂ ∧ P.degree = degree (cyclotomic' n ℂ) ∧ P.Monic) ⋯).coeff
        i
⊢ map (Int.castRingHom ℤ)
      (⋯.choose (p := fun (P : ℤ[X]) ↦
        map (Int.castRingHom ℂ) P = cyclotomic' n ℂ ∧ P.degree = degree (cyclotomic' n ℂ) ∧ P.Monic)) =
    Exists.choose (p := fun (P : ℤ[X]) ↦
      map (Int.castRingHom ℂ) P = cyclotomic' n ℂ ∧ P.degree = degree (cyclotomic' n ℂ) ∧ P.Monic) ⋯

Tactic:
ext i
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
h : n ≠ 0
i : ℕ
⊢ (map (Int.castRingHom ℤ)
          (⋯.choose (p := fun (P : ℤ[X]) ↦
            map (Int.castRingHom ℂ) P = cyclotomic' n ℂ ∧ P.degree = degree (cyclotomic' n ℂ) ∧ P.Monic))).coeff
      i =
    (Exists.choose (p := fun (P : ℤ[X]) ↦
          map (Int.castRingHom ℂ) P = cyclotomic' n ℂ ∧ P.degree = degree (cyclotomic' n ℂ) ∧ P.Monic) ⋯).coeff
      i

Tactic:
simp only [coeff_map, Int.cast_id, eq_intCast]

Premises used: Polynomial.coeff_map, eq_intCast, Int.cast_id
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
R : Type u_1
inst : Ring R
pos : ∀ (hzero : n = 0), Eq (α := R[X]) (map (Int.castRingHom R) (cyclotomic n ℤ)) (cyclotomic n R)
neg : ∀ (hzero : ¬n = 0), Eq (α := R[X]) (map (Int.castRingHom R) (cyclotomic n ℤ)) (cyclotomic n R)
⊢ Eq (α := R[X]) (map (Int.castRingHom R) (cyclotomic n ℤ)) (cyclotomic n R)

Tactic:
by_cases hzero : n = 0
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
R : Type u_1
inst : Ring R
hzero : n = 0
⊢ Eq (α := R[X]) (map (Int.castRingHom R) (cyclotomic n ℤ)) (cyclotomic n R)

Tactic:
simp only [hzero, cyclotomic, dif_pos, Polynomial.map_one]

Premises used: Polynomial.map_one, Polynomial.cyclotomic, dif_pos
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
R : Type u_1
inst : Ring R
hzero : ¬n = 0
⊢ Eq (α := R[X]) (map (Int.castRingHom R) (cyclotomic n ℤ)) (cyclotomic n R)

Tactic:
simp [cyclotomic, hzero]

Premises used: Polynomial.cyclotomic
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
pos :
  ∀ (hzero : n = 0),
    map (Int.castRingHom ℂ) (cyclotomic n ℤ) = cyclotomic' n ℂ ∧
      degree (cyclotomic n ℤ) = degree (cyclotomic' n ℂ) ∧ Monic (cyclotomic n ℤ)
neg :
  ∀ (hzero : ¬n = 0),
    map (Int.castRingHom ℂ) (cyclotomic n ℤ) = cyclotomic' n ℂ ∧
      degree (cyclotomic n ℤ) = degree (cyclotomic' n ℂ) ∧ Monic (cyclotomic n ℤ)
⊢ map (Int.castRingHom ℂ) (cyclotomic n ℤ) = cyclotomic' n ℂ ∧
    degree (cyclotomic n ℤ) = degree (cyclotomic' n ℂ) ∧ Monic (cyclotomic n ℤ)

Tactic:
by_cases hzero : n = 0
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
hzero : n = 0
⊢ map (Int.castRingHom ℂ) (cyclotomic n ℤ) = cyclotomic' n ℂ ∧
    degree (cyclotomic n ℤ) = degree (cyclotomic' n ℂ) ∧ Monic (cyclotomic n ℤ)

Tactic:
simp only [hzero, cyclotomic, degree_one, monic_one, cyclotomic'_zero, dif_pos,
      Polynomial.map_one, and_self_iff]

Premises used: Polynomial.map_one, Polynomial.cyclotomic, dif_pos, Polynomial.degree_one, and_self_iff, Polynomial.monic_one, Polynomial.cyclotomic'_zero
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
hzero : ¬n = 0
neg :
  map (Int.castRingHom ℂ)
        (Exists.choose (p := fun (P : ℤ[X]) ↦
          map (Int.castRingHom ℂ) P = cyclotomic' n ℂ ∧ P.degree = degree (cyclotomic' n ℂ) ∧ P.Monic) ⋯) =
      cyclotomic' n ℂ ∧
    (Exists.choose (p := fun (P : ℤ[X]) ↦
            map (Int.castRingHom ℂ) P = cyclotomic' n ℂ ∧ P.degree = degree (cyclotomic' n ℂ) ∧ P.Monic) ⋯).degree =
        degree (cyclotomic' n ℂ) ∧
      (Exists.choose (p := fun (P : ℤ[X]) ↦
          map (Int.castRingHom ℂ) P = cyclotomic' n ℂ ∧ P.degree = degree (cyclotomic' n ℂ) ∧ P.Monic) ⋯).Monic
⊢ map (Int.castRingHom ℂ) (cyclotomic n ℤ) = cyclotomic' n ℂ ∧
    degree (cyclotomic n ℤ) = degree (cyclotomic' n ℂ) ∧ Monic (cyclotomic n ℤ)

Tactic:
rw [int_cyclotomic_rw hzero]

Premises used: Polynomial.int_cyclotomic_rw
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
hzero : ¬n = 0
⊢ map (Int.castRingHom ℂ)
        (Exists.choose (p := fun (P : ℤ[X]) ↦
          map (Int.castRingHom ℂ) P = cyclotomic' n ℂ ∧ P.degree = degree (cyclotomic' n ℂ) ∧ P.Monic) ⋯) =
      cyclotomic' n ℂ ∧
    (Exists.choose (p := fun (P : ℤ[X]) ↦
            map (Int.castRingHom ℂ) P = cyclotomic' n ℂ ∧ P.degree = degree (cyclotomic' n ℂ) ∧ P.Monic) ⋯).degree =
        degree (cyclotomic' n ℂ) ∧
      (Exists.choose (p := fun (P : ℤ[X]) ↦
          map (Int.castRingHom ℂ) P = cyclotomic' n ℂ ∧ P.degree = degree (cyclotomic' n ℂ) ∧ P.Monic) ⋯).Monic

Tactic:
(int_coeff_of_cyclotomic' (Complex.isPrimitiveRoot_exp n hzero)).choose_spec

Premises used: Exists.choose_spec, Polynomial.int_coeff_of_cyclotomic', Complex.isPrimitiveRoot_exp
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
hzero : ¬n = 0
⊢ map (Int.castRingHom ℂ)
        (Exists.choose (p := fun (P : ℤ[X]) ↦
          map (Int.castRingHom ℂ) P = cyclotomic' n ℂ ∧ P.degree = degree (cyclotomic' n ℂ) ∧ P.Monic) ⋯) =
      cyclotomic' n ℂ ∧
    (Exists.choose (p := fun (P : ℤ[X]) ↦
            map (Int.castRingHom ℂ) P = cyclotomic' n ℂ ∧ P.degree = degree (cyclotomic' n ℂ) ∧ P.Monic) ⋯).degree =
        degree (cyclotomic' n ℂ) ∧
      (Exists.choose (p := fun (P : ℤ[X]) ↦
          map (Int.castRingHom ℂ) P = cyclotomic' n ℂ ∧ P.degree = degree (cyclotomic' n ℂ) ∧ P.Monic) ⋯).Monic

Tactic:
exact (int_coeff_of_cyclotomic' (Complex.isPrimitiveRoot_exp n hzero)).choose_spec

Premises used: Exists.choose_spec, Polynomial.int_coeff_of_cyclotomic', Complex.isPrimitiveRoot_exp
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
P : ℤ[X]
h : map (Int.castRingHom ℂ) P = cyclotomic' n ℂ
a : map (Int.castRingHom ℂ) P = map (Int.castRingHom ℂ) (cyclotomic n ℤ)
⊢ P = cyclotomic n ℤ

Tactic:
apply map_injective (Int.castRingHom ℂ) Int.cast_injective

Premises used: Polynomial.map_injective, Int.castRingHom, Complex, Int.cast_injective
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
P : ℤ[X]
h : map (Int.castRingHom ℂ) P = cyclotomic' n ℂ
a : cyclotomic' n ℂ = map (Int.castRingHom ℂ) (cyclotomic n ℤ)
a₁ a₂ : Eq (α := ℂ[X]) (cyclotomic' n ℂ) (cyclotomic' n ℂ)
⊢ map (Int.castRingHom ℂ) P = map (Int.castRingHom ℂ) (cyclotomic n ℤ)

Tactic:
rw [h, (int_cyclotomic_spec n).1]

Premises used: And.left, Polynomial.int_cyclotomic_spec
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
rw : map (f.comp (Int.castRingHom R)) (cyclotomic n ℤ) = map (Int.castRingHom S) (cyclotomic n ℤ)
⊢ map f (cyclotomic n R) = cyclotomic n S

Tactic:
rw [← map_cyclotomic_int n R, ← map_cyclotomic_int n S, map_map]

Premises used: Polynomial.map_cyclotomic_int, Polynomial.map_map
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
⊢ Subsingleton.{max (u_2 + 1) 1} (ℤ →+* S)

Tactic:
have : Subsingleton (ℤ →+* S) := inferInstance
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
this : Subsingleton.{max (u_2 + 1) 1} (ℤ →+* S)
⊢ map (f.comp (Int.castRingHom R)) (cyclotomic n ℤ) = map (Int.castRingHom S) (cyclotomic n ℤ)

Tactic:
congr!
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
S : Type u_2
q : R
n : ℕ
inst : Ring R
inst_1 : Ring S
f : R →+* S
rw :
  Eq.{u_2 + 1} (α := S) (eval ((f : (a : R) → S) q) (map f (cyclotomic n R)) : S)
    ((f : (a : R) → S) (eval q (cyclotomic n R)) : S)
rw₁ : eval₂ f ((f : (a : R) → S) q) (cyclotomic n R) = (f : (a : R) → S) (eval q (cyclotomic n R))
rw₂ rw₃ :
  Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (eval q (cyclotomic n R)) : S)
    ((f : (a : R) → S) (eval q (cyclotomic n R)) : S)
⊢ Eq.{u_2 + 1} (α := S) (eval ((f : (a : R) → S) q) (cyclotomic n S) : S)
    ((f : (a : R) → S) (eval q (cyclotomic n R)) : S)

Tactic:
rw [← map_cyclotomic n f, eval_map, eval₂_at_apply]

Premises used: Polynomial.eval_map, Polynomial.eval₂_at_apply, Polynomial.map_cyclotomic
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
q : ℝ
n : ℕ
⊢ eval (↑q : ℂ) (cyclotomic n ℂ) = (↑(eval q (cyclotomic n ℝ)) : ℂ)

Tactic:
cyclotomic.eval_apply q n (algebraMap ℝ ℂ)

Premises used: Polynomial.eval, Real, Algebra.algebraMap, Polynomial.cyclotomic.eval_apply, Complex
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : Ring R
⊢ Eq (α := R[X]) (cyclotomic 0 R) 1

Tactic:
simp only [cyclotomic, dif_pos]

Premises used: Polynomial.cyclotomic, dif_pos
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : Ring R
⊢ map (Int.castRingHom ℂ) (HSub.hSub (α := ℤ[X]) X 1) = cyclotomic' 1 ℂ

Tactic:
simp only [cyclotomic'_one, map_X, Polynomial.map_one, Polynomial.map_sub]

Premises used: Polynomial.map_one, Polynomial.cyclotomic'_one, Polynomial.map_X, Polynomial.map_sub
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : Ring R
⊢ map (Int.castRingHom ℂ) (HSub.hSub (α := ℤ[X]) X 1) = cyclotomic' 1 ℂ

Tactic:
have hspec : map (Int.castRingHom ℂ) (X - 1) = cyclotomic' 1 ℂ := by
    simp only [cyclotomic'_one, map_X, Polynomial.map_one, Polynomial.map_sub]
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : Ring R
hspec : map (Int.castRingHom ℂ) (HSub.hSub (α := ℤ[X]) X 1) = cyclotomic' 1 ℂ
symm : HSub.hSub (α := R[X]) X 1 = cyclotomic 1 R
⊢ cyclotomic 1 R = HSub.hSub (α := R[X]) X 1

Tactic:
symm
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : Ring R
hspec : map (Int.castRingHom ℂ) (HSub.hSub (α := ℤ[X]) X 1) = cyclotomic' 1 ℂ
rw : HSub.hSub (α := R[X]) X 1 = map (Int.castRingHom R) (HSub.hSub (α := ℤ[X]) X 1)
⊢ HSub.hSub (α := R[X]) X 1 = cyclotomic 1 R

Tactic:
rw [← map_cyclotomic_int, ← int_cyclotomic_unique hspec]

Premises used: Polynomial.map_cyclotomic_int, Polynomial.int_cyclotomic_unique
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : Ring R
hspec : map (Int.castRingHom ℂ) (HSub.hSub (α := ℤ[X]) X 1) = cyclotomic' 1 ℂ
⊢ HSub.hSub (α := R[X]) X 1 = map (Int.castRingHom R) (HSub.hSub (α := ℤ[X]) X 1)

Tactic:
simp only [map_X, Polynomial.map_one, Polynomial.map_sub]

Premises used: Polynomial.map_one, Polynomial.map_X, Polynomial.map_sub
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
R : Type u_1
inst : Ring R
rw : Monic.{u_1} (R := R) (map (Int.castRingHom R) (cyclotomic n ℤ))
⊢ Monic (cyclotomic n R)

Tactic:
rw [← map_cyclotomic_int]

Premises used: Polynomial.map_cyclotomic_int
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
R : Type u_1
inst : Ring R
⊢ Monic.{u_1} (R := R) (map (Int.castRingHom R) (cyclotomic n ℤ))

Tactic:
(int_cyclotomic_spec n).2.2.map _

Premises used: And.right, Polynomial.Monic.map, Polynomial.int_cyclotomic_spec
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
R : Type u_1
inst : Ring R
⊢ Monic.{u_1} (R := R) (map (Int.castRingHom R) (cyclotomic n ℤ))

Tactic:
exact (int_cyclotomic_spec n).2.2.map _

Premises used: And.right, Polynomial.Monic.map, Polynomial.int_cyclotomic_spec
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
⊢ IsPrimitive.{u_1} (R := R) (cyclotomic n R)

Tactic:
(cyclotomic.monic n R).isPrimitive

Premises used: Polynomial.cyclotomic.monic, Polynomial.Monic.isPrimitive
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
⊢ Ne (α := R[X]) (cyclotomic n R) 0

Tactic:
(cyclotomic.monic n R).ne_zero

Premises used: Polynomial.cyclotomic.monic, Polynomial.Monic.ne_zero
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
rw : degree.{u_1} (R := R) (map (Int.castRingHom R) (cyclotomic n ℤ)) = (↑n.totient : WithBot ℕ)
⊢ degree (cyclotomic n R) = (↑n.totient : WithBot ℕ)

Tactic:
rw [← map_cyclotomic_int]

Premises used: Polynomial.map_cyclotomic_int
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
rw : degree (cyclotomic n ℤ) = (↑n.totient : WithBot ℕ)
rw₁ : Ne (α := R) (((Int.castRingHom R : ℤ →+* R) : (a : ℤ) → R) (leadingCoeff (cyclotomic n ℤ)) : R) (0 : R)
⊢ degree.{u_1} (R := R) (map (Int.castRingHom R) (cyclotomic n ℤ)) = (↑n.totient : WithBot ℕ)

Tactic:
rw [degree_map_eq_of_leadingCoeff_ne_zero (Int.castRingHom R) _]

Premises used: Polynomial.degree_map_eq_of_leadingCoeff_ne_zero, Int.castRingHom
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
zero : degree (cyclotomic 0 ℤ) = (↑(Nat.totient 0) : WithBot ℕ)
succ : ∀ (k : ℕ), degree (cyclotomic (k + 1) ℤ) = (↑(k + 1).totient : WithBot ℕ)
⊢ degree (cyclotomic n ℤ) = (↑n.totient : WithBot ℕ)

Tactic:
rcases n with - | k
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
⊢ degree (cyclotomic 0 ℤ) = (↑(Nat.totient 0) : WithBot ℕ)

Tactic:
simp only [cyclotomic, degree_one, dif_pos, Nat.totient_zero, CharP.cast_eq_zero]

Premises used: CharP.cast_eq_zero, Polynomial.cyclotomic, dif_pos, Nat.totient_zero, Polynomial.degree_one
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
k : ℕ
succ : degree (cyclotomic (k + 1) ℤ) = degree (cyclotomic' k.succ ℂ)
⊢ degree (cyclotomic (k + 1) ℤ) = (↑(k + 1).totient : WithBot ℕ)

Tactic:
rw [← degree_cyclotomic' (Complex.isPrimitiveRoot_exp k.succ (Nat.succ_ne_zero k))]

Premises used: Complex.isPrimitiveRoot_exp, Nat.succ_ne_zero, Polynomial.degree_cyclotomic', Nat.succ
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
k : ℕ
⊢ degree (cyclotomic (k + 1) ℤ) = degree (cyclotomic' k.succ ℂ)

Tactic:
(int_cyclotomic_spec k.succ).2.1

Premises used: And.right, And.left, Nat.succ, Polynomial.int_cyclotomic_spec
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
k : ℕ
⊢ degree (cyclotomic (k + 1) ℤ) = degree (cyclotomic' k.succ ℂ)

Tactic:
exact (int_cyclotomic_spec k.succ).2.1

Premises used: And.right, And.left, Nat.succ, Polynomial.int_cyclotomic_spec
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
⊢ Ne (α := R) (((Int.castRingHom R : ℤ →+* R) : (a : ℤ) → R) (leadingCoeff (cyclotomic n ℤ)) : R) (0 : R)

Tactic:
simp only [(int_cyclotomic_spec n).right.right, eq_intCast, Monic.leadingCoeff, Int.cast_one,
    Ne, not_false_iff, one_ne_zero]

Premises used: Ne, eq_intCast, And.right, Polynomial.Monic.leadingCoeff, not_false_iff, one_ne_zero, Int.cast_one, Polynomial.int_cyclotomic_spec
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
rw : WithBot.unbotD 0 (↑n.totient : WithBot ℕ) = n.totient
⊢ natDegree (cyclotomic n R) = n.totient

Tactic:
rw [natDegree, degree_cyclotomic]

Premises used: Polynomial.natDegree, Polynomial.degree_cyclotomic
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
⊢ WithBot.unbotD 0 (↑n.totient : WithBot ℕ) = n.totient

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : Ring R
n : ℕ
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h : Nontrivial R
rw rw₁ : n.totient ≤ n.totient
⊢ natDegree (cyclotomic n R) ≤ n.totient

Tactic:
rw [natDegree_cyclotomic]

Premises used: Polynomial.natDegree_cyclotomic
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
R : Type u_1
hpos : 0 < n
inst : Ring R
inst_1 : Nontrivial R
rwa : LT.lt (α := WithBot ℕ) 0 (↑n.totient : WithBot ℕ)
rwa₁ : 0 < n.totient
rwa₂ rwa₃ rwa₄ rwa₅ : 0 < n
⊢ 0 < degree (cyclotomic n R)

Tactic:
rwa [degree_cyclotomic n R, Nat.cast_pos, Nat.totient_pos]

Premises used: Nat.cast_pos, Nat.totient_pos, Polynomial.degree_cyclotomic
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
hpos : 0 < n
R : Type u_1
inst : CommRing R
a : map (Int.castRingHom ℂ) (∏ i ∈ n.divisors, cyclotomic i ℤ) = map (Int.castRingHom ℂ) (HPow.hPow (α := ℤ[X]) X n - 1)
⊢ ∏ i ∈ n.divisors, cyclotomic i ℤ = HPow.hPow (α := ℤ[X]) X n - 1

Tactic:
apply map_injective (Int.castRingHom ℂ) Int.cast_injective

Premises used: Polynomial.map_injective, Int.castRingHom, Complex, Int.cast_injective
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
hpos : 0 < n
R : Type u_1
inst : CommRing R
a : ∏ x ∈ n.divisors, cyclotomic' x ℂ = HPow.hPow (α := ℂ[X]) X n - 1
⊢ map (Int.castRingHom ℂ) (∏ i ∈ n.divisors, cyclotomic i ℤ) = map (Int.castRingHom ℂ) (HPow.hPow (α := ℤ[X]) X n - 1)

Tactic:
simp only [Polynomial.map_prod, int_cyclotomic_spec, Polynomial.map_pow, map_X,
      Polynomial.map_one, Polynomial.map_sub]

Premises used: Polynomial.map_one, Polynomial.map_pow, Polynomial.map_X, Polynomial.map_prod, Polynomial.map_sub, Polynomial.int_cyclotomic_spec
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
hpos : 0 < n
R : Type u_1
inst : CommRing R
⊢ ∏ x ∈ n.divisors, cyclotomic' x ℂ = HPow.hPow (α := ℂ[X]) X n - 1

Tactic:
prod_cyclotomic'_eq_X_pow_sub_one hpos (Complex.isPrimitiveRoot_exp n hpos.ne')

Premises used: Polynomial.prod_cyclotomic'_eq_X_pow_sub_one, Complex.isPrimitiveRoot_exp, LT.lt.ne'
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
hpos : 0 < n
R : Type u_1
inst : CommRing R
⊢ ∏ x ∈ n.divisors, cyclotomic' x ℂ = HPow.hPow (α := ℂ[X]) X n - 1

Tactic:
exact prod_cyclotomic'_eq_X_pow_sub_one hpos (Complex.isPrimitiveRoot_exp n hpos.ne')

Premises used: Polynomial.prod_cyclotomic'_eq_X_pow_sub_one, Complex.isPrimitiveRoot_exp, LT.lt.ne'
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
hpos : 0 < n
R : Type u_1
inst : CommRing R
⊢ ∏ i ∈ n.divisors, cyclotomic i ℤ = HPow.hPow (α := ℤ[X]) X n - 1

Tactic:
have integer : ∏ i ∈ Nat.divisors n, cyclotomic i ℤ = X ^ n - 1 := by
    apply map_injective (Int.castRingHom ℂ) Int.cast_injective
    simp only [Polynomial.map_prod, int_cyclotomic_spec, Polynomial.map_pow, map_X,
      Polynomial.map_one, Polynomial.map_sub]
    exact prod_cyclotomic'_eq_X_pow_sub_one hpos (Complex.isPrimitiveRoot_exp n hpos.ne')
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
hpos : 0 < n
R : Type u_1
inst : CommRing R
integer : ∏ i ∈ n.divisors, cyclotomic i ℤ = HPow.hPow (α := ℤ[X]) X n - 1
⊢ ∏ i ∈ n.divisors, cyclotomic i R = HPow.hPow (α := R[X]) X n - 1

Tactic:
simpa only [Polynomial.map_prod, map_cyclotomic_int, Polynomial.map_sub, Polynomial.map_one,
    Polynomial.map_pow, Polynomial.map_X] using congr_arg (map (Int.castRingHom R)) integer

Premises used: Polynomial.map_one, Polynomial.map_pow, Polynomial.map_X, congr_arg, Polynomial.map_prod, Int.castRingHom, Polynomial.map_cyclotomic_int, Polynomial.map_sub, Polynomial.map
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
R : Type u_1
inst : Ring R
this : cyclotomic n ℤ ∣ HPow.hPow (α := ℤ[X]) X n - 1
⊢ cyclotomic n R ∣ HPow.hPow (α := R[X]) X n - 1

Tactic:
simpa only [map_cyclotomic_int, Polynomial.map_sub, Polynomial.map_one, Polynomial.map_pow,
      Polynomial.map_X] using Polynomial.map_dvd (Int.castRingHom R) this

Premises used: Polynomial.map_one, Polynomial.map_dvd, Polynomial.map_pow, Polynomial.map_X, Int.castRingHom, Polynomial.map_cyclotomic_int, Polynomial.map_sub
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
R : Type u_1
inst : Ring R
suffices : cyclotomic n ℤ ∣ HPow.hPow (α := ℤ[X]) X n - 1
⊢ cyclotomic n R ∣ HPow.hPow (α := R[X]) X n - 1

Tactic:
suffices cyclotomic n ℤ ∣ X ^ n - 1 by
    simpa only [map_cyclotomic_int, Polynomial.map_sub, Polynomial.map_one, Polynomial.map_pow,
      Polynomial.map_X] using Polynomial.map_dvd (Int.castRingHom R) this
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
R : Type u_1
inst : Ring R
inl : cyclotomic 0 ℤ ∣ HPow.hPow (α := ℤ[X]) (β := ℕ) X 0 - 1
inr : ∀ (hn : n > 0), cyclotomic n ℤ ∣ HPow.hPow (α := ℤ[X]) X n - 1
⊢ cyclotomic n ℤ ∣ HPow.hPow (α := ℤ[X]) X n - 1

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

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : Ring R
⊢ cyclotomic 0 ℤ ∣ HPow.hPow (α := ℤ[X]) (β := ℕ) X 0 - 1

Tactic:
simp