awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
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 = cyclotomic 1 R
have rw : HSub.hSub (α := R[X]) X 1 = map (Int.castRingHom R) (HSub.hSub (α := ℤ[X]) X 1)
Tactic: rw [← map_cyclotomic_int, ← int_cyclotomic_unique hspec]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
R : Type u_1
inst : Ring R
⊢ Monic (cyclotomic n R)
have rw : Monic.{u_1} (R := R) (map (Int.castRingHom R) (cyclotomic n ℤ))
Tactic: rw [← map_cyclotomic_int]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
⊢ degree (cyclotomic n R) = (↑n.totient : WithBot ℕ)
have rw : degree.{u_1} (R := R) (map (Int.castRingHom R) (cyclotomic n ℤ)) = (↑n.totient : WithBot ℕ)
Tactic: rw [← map_cyclotomic_int]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
⊢ degree.{u_1} (R := R) (map (Int.castRingHom R) (cyclotomic n ℤ)) = (↑n.totient : WithBot ℕ)
have rw : degree (cyclotomic n ℤ) = (↑n.totient : WithBot ℕ)
Tactic: rw [degree_map_eq_of_leadingCoeff_ne_zero (Int.castRingHom R) _]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
rw : degree (cyclotomic n ℤ) = (↑n.totient : WithBot ℕ)
⊢ degree.{u_1} (R := R) (map (Int.castRingHom R) (cyclotomic n ℤ)) = (↑n.totient : WithBot ℕ)
have rw₁ : Ne (α := R) (((Int.castRingHom R : ℤ →+* R) : (a : ℤ) → R) (leadingCoeff (cyclotomic n ℤ)) : R) (0 : R)
Tactic: rw [degree_map_eq_of_leadingCoeff_ne_zero (Int.castRingHom R) _]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
⊢ degree (cyclotomic n ℤ) = (↑n.totient : WithBot ℕ)
have zero : degree (cyclotomic 0 ℤ) = (↑(Nat.totient 0) : WithBot ℕ)
Tactic: rcases n with - | k
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
zero : degree (cyclotomic 0 ℤ) = (↑(Nat.totient 0) : WithBot ℕ)
⊢ degree (cyclotomic n ℤ) = (↑n.totient : WithBot ℕ)
have succ : ∀ (k : ℕ), degree (cyclotomic (k + 1) ℤ) = (↑(k + 1).totient : WithBot ℕ)
Tactic: rcases n with - | k
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
k : ℕ
⊢ degree (cyclotomic (k + 1) ℤ) = (↑(k + 1).totient : WithBot ℕ)
have succ : degree (cyclotomic (k + 1) ℤ) = degree (cyclotomic' k.succ ℂ)
Tactic: rw [← degree_cyclotomic' (Complex.isPrimitiveRoot_exp k.succ (Nat.succ_ne_zero k))]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
⊢ natDegree (cyclotomic n R) = n.totient
have rw : WithBot.unbotD 0 (↑n.totient : WithBot ℕ) = n.totient
Tactic: rw [natDegree, degree_cyclotomic]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (hypothesis)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
⊢ natDegree (cyclotomic n R) ≤ n.totient
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h : Nontrivial R
⊢ natDegree (cyclotomic n R) ≤ n.totient
have rw : n.totient ≤ n.totient
Tactic: rw [natDegree_cyclotomic]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
R : Type u_1
hpos : 0 < n
inst : Ring R
inst_1 : Nontrivial R
⊢ 0 < degree (cyclotomic n R)
have rwa : LT.lt (α := WithBot ℕ) 0 (↑n.totient : WithBot ℕ)
Tactic: rwa [degree_cyclotomic n R, Nat.cast_pos, Nat.totient_pos]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
R : Type u_1
hpos : 0 < n
inst : Ring R
inst_1 : Nontrivial R
rwa : LT.lt (α := WithBot ℕ) 0 (↑n.totient : WithBot ℕ)
⊢ 0 < degree (cyclotomic n R)
have rwa₁ : 0 < n.totient
Tactic: rwa [degree_cyclotomic n R, Nat.cast_pos, Nat.totient_pos]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
hpos : 0 < n
R : Type u_1
inst : CommRing R
⊢ ∏ i ∈ n.divisors, cyclotomic i ℤ = HPow.hPow (α := ℤ[X]) X n - 1
have a : map (Int.castRingHom ℂ) (∏ i ∈ n.divisors, cyclotomic i ℤ) = map (Int.castRingHom ℂ) (HPow.hPow (α := ℤ[X]) X n - 1)
Tactic: apply map_injective (Int.castRingHom ℂ) Int.cast_injective
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
hpos : 0 < n
R : Type u_1
inst : CommRing R
⊢ map (Int.castRingHom ℂ) (∏ i ∈ n.divisors, cyclotomic i ℤ) = map (Int.castRingHom ℂ) (HPow.hPow (α := ℤ[X]) X n - 1)
have a : ∏ x ∈ n.divisors, cyclotomic' x ℂ = 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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (hypothesis)
Goal:
n : ℕ
hpos : 0 < n
R : Type u_1
inst : CommRing R
⊢ ∏ i ∈ n.divisors, cyclotomic i R = HPow.hPow (α := R[X]) X n - 1
have integer : ∏ 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')
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
R : Type u_1
inst : Ring R
⊢ cyclotomic n R ∣ HPow.hPow (α := R[X]) X n - 1
have suffices : cyclotomic n ℤ ∣ HPow.hPow (α := ℤ[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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
R : Type u_1
inst : Ring R
⊢ cyclotomic n ℤ ∣ HPow.hPow (α := ℤ[X]) X n - 1
have inl : cyclotomic 0 ℤ ∣ HPow.hPow (α := ℤ[X]) (β := ℕ) X 0 - 1
Tactic: rcases n.eq_zero_or_pos with (rfl | hn)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
R : Type u_1
inst : Ring R
inl : cyclotomic 0 ℤ ∣ HPow.hPow (α := ℤ[X]) (β := ℕ) X 0 - 1
⊢ cyclotomic n ℤ ∣ HPow.hPow (α := ℤ[X]) X n - 1
have inr : ∀ (hn : n > 0), cyclotomic n ℤ ∣ HPow.hPow (α := ℤ[X]) X n - 1
Tactic: rcases n.eq_zero_or_pos with (rfl | hn)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
R : Type u_1
inst : Ring R
hn : n > 0
⊢ cyclotomic n ℤ ∣ HPow.hPow (α := ℤ[X]) X n - 1
have inr : Dvd.dvd (α := ℤ[X]) (cyclotomic n ℤ) (∏ i ∈ n.divisors, cyclotomic i ℤ)
Tactic: rw [← prod_cyclotomic_eq_X_pow_sub_one hn]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
h : 0 < n
R : Type u_1
inst : CommRing R
⊢ Eq.{u_1 + 1} (α := R[X]) (∏ i ∈ n.divisors.erase 1, cyclotomic i R) (∑ i ∈ range n, HPow.hPow (α := R[X]) X i)
have suffices : Eq (α := ℤ[X]) (∏ i ∈ n.divisors.erase 1, cyclotomic i ℤ) (∑ i ∈ range n, HPow.hPow (α := ℤ[X]) X i)
Tactic: suffices (∏ i ∈ n.divisors.erase 1, cyclotomic i ℤ) = ∑ i ∈ Finset.range n, X ^ i by
    simpa only [Polynomial.map_prod, map_cyclotomic_int, Polynomial.map_sum, Polynomial.map_pow,
      Polynomial.map_X] using congr_arg (map (Int.castRingHom R)) this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
h : 0 < n
R : Type u_1
inst : CommRing R
⊢ Eq (α := ℤ[X]) (∏ i ∈ n.divisors.erase 1, cyclotomic i ℤ) (∑ i ∈ range n, HPow.hPow (α := ℤ[X]) X i)
have rw : HMul.hMul (α := ℤ[X]) (∏ i ∈ n.divisors.erase 1, cyclotomic i ℤ) (cyclotomic 1 ℤ) =
  HMul.hMul (α := ℤ[X]) (∑ i ∈ range n, HPow.hPow (α := ℤ[X]) X i) (cyclotomic 1 ℤ)
Tactic: rw [← mul_left_inj' (cyclotomic_ne_zero 1 ℤ), prod_erase_mul _ _ (Nat.one_mem_divisors.2 h.ne'),
    cyclotomic_one, geom_sum_mul, prod_cyclotomic_eq_X_pow_sub_one h]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
h : 0 < n
R : Type u_1
inst : CommRing R
rw :
  HMul.hMul (α := ℤ[X]) (∏ i ∈ n.divisors.erase 1, cyclotomic i ℤ) (cyclotomic 1 ℤ) =
    HMul.hMul (α := ℤ[X]) (∑ i ∈ range n, HPow.hPow (α := ℤ[X]) X i) (cyclotomic 1 ℤ)
⊢ Eq (α := ℤ[X]) (∏ i ∈ n.divisors.erase 1, cyclotomic i ℤ) (∑ i ∈ range n, HPow.hPow (α := ℤ[X]) X i)
have rw₁ : ∏ x ∈ n.divisors, cyclotomic x ℤ = HMul.hMul (α := ℤ[X]) (∑ i ∈ range n, HPow.hPow (α := ℤ[X]) X i) (cyclotomic 1 ℤ)
Tactic: rw [← mul_left_inj' (cyclotomic_ne_zero 1 ℤ), prod_erase_mul _ _ (Nat.one_mem_divisors.2 h.ne'),
    cyclotomic_one, geom_sum_mul, prod_cyclotomic_eq_X_pow_sub_one h]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
h : 0 < n
R : Type u_1
inst : CommRing R
rw :
  HMul.hMul (α := ℤ[X]) (∏ i ∈ n.divisors.erase 1, cyclotomic i ℤ) (cyclotomic 1 ℤ) =
    HMul.hMul (α := ℤ[X]) (∑ i ∈ range n, HPow.hPow (α := ℤ[X]) X i) (cyclotomic 1 ℤ)
rw₁ :
  ∏ x ∈ n.divisors, cyclotomic x ℤ = HMul.hMul (α := ℤ[X]) (∑ i ∈ range n, HPow.hPow (α := ℤ[X]) X i) (cyclotomic 1 ℤ)
⊢ Eq (α := ℤ[X]) (∏ i ∈ n.divisors.erase 1, cyclotomic i ℤ) (∑ i ∈ range n, HPow.hPow (α := ℤ[X]) X i)
have rw₂ : ∏ x ∈ n.divisors, cyclotomic x ℤ = (∑ i ∈ range n, HPow.hPow (α := ℤ[X]) X i) * HSub.hSub (α := ℤ[X]) X 1
Tactic: rw [← mul_left_inj' (cyclotomic_ne_zero 1 ℤ), prod_erase_mul _ _ (Nat.one_mem_divisors.2 h.ne'),
    cyclotomic_one, geom_sum_mul, prod_cyclotomic_eq_X_pow_sub_one h]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
h : 0 < n
R : Type u_1
inst : CommRing R
rw :
  HMul.hMul (α := ℤ[X]) (∏ i ∈ n.divisors.erase 1, cyclotomic i ℤ) (cyclotomic 1 ℤ) =
    HMul.hMul (α := ℤ[X]) (∑ i ∈ range n, HPow.hPow (α := ℤ[X]) X i) (cyclotomic 1 ℤ)
rw₁ :
  ∏ x ∈ n.divisors, cyclotomic x ℤ = HMul.hMul (α := ℤ[X]) (∑ i ∈ range n, HPow.hPow (α := ℤ[X]) X i) (cyclotomic 1 ℤ)
rw₂ : ∏ x ∈ n.divisors, cyclotomic x ℤ = (∑ i ∈ range n, HPow.hPow (α := ℤ[X]) X i) * HSub.hSub (α := ℤ[X]) X 1
⊢ Eq (α := ℤ[X]) (∏ i ∈ n.divisors.erase 1, cyclotomic i ℤ) (∑ i ∈ range n, HPow.hPow (α := ℤ[X]) X i)
have rw₃ : ∏ x ∈ n.divisors, cyclotomic x ℤ = HPow.hPow (α := ℤ[X]) X n - 1
Tactic: rw [← mul_left_inj' (cyclotomic_ne_zero 1 ℤ), prod_erase_mul _ _ (Nat.one_mem_divisors.2 h.ne'),
    cyclotomic_one, geom_sum_mul, prod_cyclotomic_eq_X_pow_sub_one h]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
h : 0 < n
R : Type u_1
inst : CommRing R
rw :
  HMul.hMul (α := ℤ[X]) (∏ i ∈ n.divisors.erase 1, cyclotomic i ℤ) (cyclotomic 1 ℤ) =
    HMul.hMul (α := ℤ[X]) (∑ i ∈ range n, HPow.hPow (α := ℤ[X]) X i) (cyclotomic 1 ℤ)
rw₁ :
  ∏ x ∈ n.divisors, cyclotomic x ℤ = HMul.hMul (α := ℤ[X]) (∑ i ∈ range n, HPow.hPow (α := ℤ[X]) X i) (cyclotomic 1 ℤ)
rw₂ : ∏ x ∈ n.divisors, cyclotomic x ℤ = (∑ i ∈ range n, HPow.hPow (α := ℤ[X]) X i) * HSub.hSub (α := ℤ[X]) X 1
rw₃ : ∏ x ∈ n.divisors, cyclotomic x ℤ = HPow.hPow (α := ℤ[X]) X n - 1
⊢ Eq (α := ℤ[X]) (∏ i ∈ n.divisors.erase 1, cyclotomic i ℤ) (∑ i ∈ range n, HPow.hPow (α := ℤ[X]) X i)
have rw₄ : HPow.hPow (α := ℤ[X]) X n - 1 = HPow.hPow (α := ℤ[X]) X n - 1
Tactic: rw [← mul_left_inj' (cyclotomic_ne_zero 1 ℤ), prod_erase_mul _ _ (Nat.one_mem_divisors.2 h.ne'),
    cyclotomic_one, geom_sum_mul, prod_cyclotomic_eq_X_pow_sub_one h]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Eq (α := R[X]) (cyclotomic p R) (∑ i ∈ range p, HPow.hPow (α := R[X]) X i)
have suffices : Eq (α := ℤ[X]) (cyclotomic p ℤ) (∑ i ∈ range p, HPow.hPow (α := ℤ[X]) X i)
Tactic: suffices cyclotomic p ℤ = ∑ i ∈ range p, X ^ i by
    simpa only [map_cyclotomic_int, Polynomial.map_sum, Polynomial.map_pow, Polynomial.map_X] using
      congr_arg (map (Int.castRingHom R)) this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Eq (α := ℤ[X]) (cyclotomic p ℤ) (∑ i ∈ range p, HPow.hPow (α := ℤ[X]) X i)
have rw : Eq (α := ℤ[X]) (cyclotomic p ℤ) (∏ i ∈ p.divisors.erase 1, cyclotomic i ℤ)
Tactic: rw [← prod_cyclotomic_eq_geom_sum hp.out.pos, hp.out.divisors,
    erase_insert (mem_singleton.not.2 hp.out.ne_one.symm), prod_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
p : ℕ
hp : Fact (Nat.Prime p)
rw : Eq (α := ℤ[X]) (cyclotomic p ℤ) (∏ i ∈ p.divisors.erase 1, cyclotomic i ℤ)
⊢ Eq (α := ℤ[X]) (cyclotomic p ℤ) (∑ i ∈ range p, HPow.hPow (α := ℤ[X]) X i)
have rw₁ : Eq (α := ℤ[X]) (cyclotomic p ℤ) (∏ i ∈ Finset.erase {1, p} 1, cyclotomic i ℤ)
Tactic: rw [← prod_cyclotomic_eq_geom_sum hp.out.pos, hp.out.divisors,
    erase_insert (mem_singleton.not.2 hp.out.ne_one.symm), prod_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
p : ℕ
hp : Fact (Nat.Prime p)
rw : Eq (α := ℤ[X]) (cyclotomic p ℤ) (∏ i ∈ p.divisors.erase 1, cyclotomic i ℤ)
rw₁ : Eq (α := ℤ[X]) (cyclotomic p ℤ) (∏ i ∈ Finset.erase {1, p} 1, cyclotomic i ℤ)
⊢ Eq (α := ℤ[X]) (cyclotomic p ℤ) (∑ i ∈ range p, HPow.hPow (α := ℤ[X]) X i)
have rw₂ : Eq (α := ℤ[X]) (cyclotomic p ℤ) (∏ i ∈ {p}, cyclotomic i ℤ)
Tactic: rw [← prod_cyclotomic_eq_geom_sum hp.out.pos, hp.out.divisors,
    erase_insert (mem_singleton.not.2 hp.out.ne_one.symm), prod_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
p : ℕ
hp : Fact (Nat.Prime p)
rw : Eq (α := ℤ[X]) (cyclotomic p ℤ) (∏ i ∈ p.divisors.erase 1, cyclotomic i ℤ)
rw₁ : Eq (α := ℤ[X]) (cyclotomic p ℤ) (∏ i ∈ Finset.erase {1, p} 1, cyclotomic i ℤ)
rw₂ : Eq (α := ℤ[X]) (cyclotomic p ℤ) (∏ i ∈ {p}, cyclotomic i ℤ)
⊢ Eq (α := ℤ[X]) (cyclotomic p ℤ) (∑ i ∈ range p, HPow.hPow (α := ℤ[X]) X i)
have rw₃ : cyclotomic p ℤ = cyclotomic p ℤ
Tactic: rw [← prod_cyclotomic_eq_geom_sum hp.out.pos, hp.out.divisors,
    erase_insert (mem_singleton.not.2 hp.out.ne_one.symm), prod_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
p : ℕ
hn : Fact (Nat.Prime p)
⊢ cyclotomic p R * HSub.hSub (α := R[X]) X 1 = HPow.hPow (α := R[X]) X p - 1
have rw : (∑ i ∈ range p, HPow.hPow (α := R[X]) X i) * HSub.hSub (α := R[X]) X 1 = HPow.hPow (α := R[X]) X p - 1
Tactic: rw [cyclotomic_prime, geom_sum_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
p : ℕ
hn : Fact (Nat.Prime p)
rw : (∑ i ∈ range p, HPow.hPow (α := R[X]) X i) * HSub.hSub (α := R[X]) X 1 = HPow.hPow (α := R[X]) X p - 1
⊢ cyclotomic p R * HSub.hSub (α := R[X]) X 1 = HPow.hPow (α := R[X]) X p - 1
have rw₁ : HPow.hPow (α := R[X]) X p - 1 = HPow.hPow (α := R[X]) X p - 1
Tactic: rw [cyclotomic_prime, geom_sum_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
d n : ℕ
hdn : d ∣ n
hd : d ≠ 1
⊢ Dvd.dvd (α := R[X]) (cyclotomic d R) (∑ i ∈ range n, HPow.hPow (α := R[X]) X i)
have suffices : Dvd.dvd (α := ℤ[X]) (cyclotomic d ℤ) (∑ i ∈ range n, HPow.hPow (α := ℤ[X]) X i)
Tactic: suffices cyclotomic d ℤ ∣ ∑ i ∈ Finset.range n, X ^ i by
    simpa only [map_cyclotomic_int, Polynomial.map_sum, Polynomial.map_pow, Polynomial.map_X] using
      map_dvd (Int.castRingHom R) this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
d n : ℕ
hdn : d ∣ n
hd : d ≠ 1
⊢ Dvd.dvd (α := ℤ[X]) (cyclotomic d ℤ) (∑ i ∈ range n, HPow.hPow (α := ℤ[X]) X i)
have inl : ∀ (hdn : d ∣ 0), Dvd.dvd (α := ℤ[X]) (cyclotomic d ℤ) (∑ i ∈ range 0, HPow.hPow (α := ℤ[X]) X i)
Tactic: rcases n.eq_zero_or_pos with (rfl | hn)
Cleared hypotheses: n, hdn
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
d n : ℕ
hdn : d ∣ n
hd : d ≠ 1
inl : ∀ (hdn : d ∣ 0), Dvd.dvd (α := ℤ[X]) (cyclotomic d ℤ) (∑ i ∈ range 0, HPow.hPow (α := ℤ[X]) X i)
⊢ Dvd.dvd (α := ℤ[X]) (cyclotomic d ℤ) (∑ i ∈ range n, HPow.hPow (α := ℤ[X]) X i)
have inr : ∀ (hn : n > 0), Dvd.dvd (α := ℤ[X]) (cyclotomic d ℤ) (∑ i ∈ range n, HPow.hPow (α := ℤ[X]) X i)
Tactic: rcases n.eq_zero_or_pos with (rfl | hn)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
d n : ℕ
hdn : d ∣ n
hd : d ≠ 1
hn : n > 0
⊢ Dvd.dvd (α := ℤ[X]) (cyclotomic d ℤ) (∑ i ∈ range n, HPow.hPow (α := ℤ[X]) X i)
have inr : Dvd.dvd (α := ℤ[X]) (cyclotomic d ℤ) (∏ i ∈ n.divisors.erase 1, cyclotomic i ℤ)
Tactic: rw [← prod_cyclotomic_eq_geom_sum hn]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
d n : ℕ
hdn : d ∣ n
hd : d ≠ 1
hn : n > 0
⊢ Dvd.dvd (α := ℤ[X]) (cyclotomic d ℤ) (∏ i ∈ n.divisors.erase 1, cyclotomic i ℤ)
have inr : d ∈ n.divisors.erase 1
Tactic: apply Finset.dvd_prod_of_mem
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
d n : ℕ
hdvd : d ∣ n
hn : n ≠ 0
⊢ (HPow.hPow (α := R[X]) X d - 1) * ∏ x ∈ n.divisors \ d.divisors, cyclotomic x R = HPow.hPow (α := R[X]) X n - 1
have h0d : 0 < d
Tactic: have h0d : 0 < d := Nat.pos_of_dvd_of_pos hdvd (by positivity)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
d n : ℕ
hdvd : d ∣ n
hn : n ≠ 0
h0d : 0 < d
⊢ (HPow.hPow (α := R[X]) X d - 1) * ∏ x ∈ n.divisors \ d.divisors, cyclotomic x R = HPow.hPow (α := R[X]) X n - 1
have rw : HMul.hMul (α := R[X]) (∏ i ∈ d.divisors, cyclotomic i R) (∏ x ∈ n.divisors \ d.divisors, cyclotomic x R) =
  HPow.hPow (α := R[X]) X n - 1
Tactic: rw [← prod_cyclotomic_eq_X_pow_sub_one h0d,
    ← prod_cyclotomic_eq_X_pow_sub_one (by positivity), mul_comm,
    Finset.prod_sdiff (by gcongr)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
d n : ℕ
hdvd : d ∣ n
hn : n ≠ 0
h0d : 0 < d
rw :
  HMul.hMul (α := R[X]) (∏ i ∈ d.divisors, cyclotomic i R) (∏ x ∈ n.divisors \ d.divisors, cyclotomic x R) =
    HPow.hPow (α := R[X]) X n - 1
⊢ (HPow.hPow (α := R[X]) X d - 1) * ∏ x ∈ n.divisors \ d.divisors, cyclotomic x R = HPow.hPow (α := R[X]) X n - 1
have rw₁ : HMul.hMul (α := R[X]) (∏ i ∈ d.divisors, cyclotomic i R) (∏ x ∈ n.divisors \ d.divisors, cyclotomic x R) =
  ∏ i ∈ n.divisors, cyclotomic i R
Tactic: rw [← prod_cyclotomic_eq_X_pow_sub_one h0d,
    ← prod_cyclotomic_eq_X_pow_sub_one (by positivity), mul_comm,
    Finset.prod_sdiff (by gcongr)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
d n : ℕ
hdvd : d ∣ n
hn : n ≠ 0
h0d : 0 < d
rw :
  HMul.hMul (α := R[X]) (∏ i ∈ d.divisors, cyclotomic i R) (∏ x ∈ n.divisors \ d.divisors, cyclotomic x R) =
    HPow.hPow (α := R[X]) X n - 1
rw₁ :
  HMul.hMul (α := R[X]) (∏ i ∈ d.divisors, cyclotomic i R) (∏ x ∈ n.divisors \ d.divisors, cyclotomic x R) =
    ∏ i ∈ n.divisors, cyclotomic i R
⊢ (HPow.hPow (α := R[X]) X d - 1) * ∏ x ∈ n.divisors \ d.divisors, cyclotomic x R = HPow.hPow (α := R[X]) X n - 1
have rw₂ : HMul.hMul (α := R[X]) (∏ x ∈ n.divisors \ d.divisors, cyclotomic x R) (∏ i ∈ d.divisors, cyclotomic i R) =
  ∏ i ∈ n.divisors, cyclotomic i R
Tactic: rw [← prod_cyclotomic_eq_X_pow_sub_one h0d,
    ← prod_cyclotomic_eq_X_pow_sub_one (by positivity), mul_comm,
    Finset.prod_sdiff (by gcongr)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
d n : ℕ
hdvd : d ∣ n
hn : n ≠ 0
h0d : 0 < d
rw :
  HMul.hMul (α := R[X]) (∏ i ∈ d.divisors, cyclotomic i R) (∏ x ∈ n.divisors \ d.divisors, cyclotomic x R) =
    HPow.hPow (α := R[X]) X n - 1
rw₁ :
  HMul.hMul (α := R[X]) (∏ i ∈ d.divisors, cyclotomic i R) (∏ x ∈ n.divisors \ d.divisors, cyclotomic x R) =
    ∏ i ∈ n.divisors, cyclotomic i R
rw₂ :
  HMul.hMul (α := R[X]) (∏ x ∈ n.divisors \ d.divisors, cyclotomic x R) (∏ i ∈ d.divisors, cyclotomic i R) =
    ∏ i ∈ n.divisors, cyclotomic i R
⊢ (HPow.hPow (α := R[X]) X d - 1) * ∏ x ∈ n.divisors \ d.divisors, cyclotomic x R = HPow.hPow (α := R[X]) X n - 1
have rw₃ : Eq.{u_1 + 1} (α := R[X]) (∏ x ∈ n.divisors, cyclotomic x R) (∏ i ∈ n.divisors, cyclotomic i R)
Tactic: rw [← prod_cyclotomic_eq_X_pow_sub_one h0d,
    ← prod_cyclotomic_eq_X_pow_sub_one (by positivity), mul_comm,
    Finset.prod_sdiff (by gcongr)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
d n : ℕ
h : d ∈ n.properDivisors
⊢ (HPow.hPow (α := R[X]) X d - 1) * cyclotomic n R ∣ HPow.hPow (α := R[X]) X n - 1
have h₁ : d ∣ n ∧ d < n
Tactic: rw [Nat.mem_properDivisors] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
d n : ℕ
h : d ∣ n ∧ d < n
⊢ (HPow.hPow (α := R[X]) X d - 1) * cyclotomic n R ∣ HPow.hPow (α := R[X]) X n - 1
have h₁ : HPow.hPow (α := R[X]) X n - 1 =
  (HPow.hPow (α := R[X]) X d - 1) * cyclotomic n R * ∏ x ∈ n.properDivisors \ d.divisors, cyclotomic x R
Tactic: use ∏ x ∈ n.properDivisors \ d.divisors, cyclotomic x R
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
d n : ℕ
h : d ∣ n ∧ d < n
⊢ HPow.hPow (α := R[X]) X n - 1 =
    (HPow.hPow (α := R[X]) X d - 1) * cyclotomic n R * ∏ x ∈ n.properDivisors \ d.divisors, cyclotomic x R
have h₁ : n ∉ n.properDivisors \ d.divisors
Tactic: rw [← X_pow_sub_one_mul_prod_cyclotomic_eq_X_pow_sub_one_of_dvd R h.1 h.2.ne_bot,
    ← Nat.insert_self_properDivisors, Finset.insert_sdiff_of_notMem,
    Finset.prod_insert, mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
d n : ℕ
h : d ∣ n ∧ d < n
h₁ : n ∉ n.properDivisors \ d.divisors
⊢ HPow.hPow (α := R[X]) X n - 1 =
    (HPow.hPow (α := R[X]) X d - 1) * cyclotomic n R * ∏ x ∈ n.properDivisors \ d.divisors, cyclotomic x R
have h₂ : n ∉ d.divisors
Tactic: rw [← X_pow_sub_one_mul_prod_cyclotomic_eq_X_pow_sub_one_of_dvd R h.1 h.2.ne_bot,
    ← Nat.insert_self_properDivisors, Finset.insert_sdiff_of_notMem,
    Finset.prod_insert, mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
d n : ℕ
h : d ∣ n ∧ d < n
h₁ : n ∉ n.properDivisors \ d.divisors
h₂ : n ∉ d.divisors
⊢ HPow.hPow (α := R[X]) X n - 1 =
    (HPow.hPow (α := R[X]) X d - 1) * cyclotomic n R * ∏ x ∈ n.properDivisors \ d.divisors, cyclotomic x R
have h₃ : n ≠ 0
Tactic: rw [← X_pow_sub_one_mul_prod_cyclotomic_eq_X_pow_sub_one_of_dvd R h.1 h.2.ne_bot,
    ← Nat.insert_self_properDivisors, Finset.insert_sdiff_of_notMem,
    Finset.prod_insert, mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
⊢ Eq (α := RatFunc R) ((algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (cyclotomic n R) : RatFunc R)
    (∏ i ∈ n.divisorsAntidiagonal,
        HPow.hPow (α := RatFunc R) (β := ℤ)
          ((algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (HPow.hPow (α := R[X]) X i.2 - 1) : RatFunc R)
          ((μ : (a : ℕ) → ℤ) i.1 : ℤ) :
      RatFunc R)
have inl : Eq (α := RatFunc R) ((algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (cyclotomic 0 R) : RatFunc R)
  (∏ i ∈ Nat.divisorsAntidiagonal 0,
      HPow.hPow (α := RatFunc R) (β := ℤ)
        ((algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (HPow.hPow (α := R[X]) X i.2 - 1) : RatFunc R)
        ((μ : (a : ℕ) → ℤ) i.1 : ℤ) :
    RatFunc R)
Tactic: rcases n.eq_zero_or_pos with (rfl | hpos)
Cleared hypotheses: n