English
If n is not a prime power, then eval 1 cyclotomic(n, R) = 1.
Русский
Если n не является степенью простого, то eval 1 cyclotomic(n, R) = 1.
LaTeX
$$eval(1, cyclotomic(n, R)) = 1$$
Lean4
theorem eval_one_cyclotomic_not_prime_pow {R : Type*} [Ring R] {n : ℕ} (h : ∀ {p : ℕ}, p.Prime → ∀ k : ℕ, p ^ k ≠ n) :
eval 1 (cyclotomic n R) = 1 := by
rcases n.eq_zero_or_pos with (rfl | hn')
· simp
have hn : 1 < n := one_lt_iff_ne_zero_and_ne_one.mpr ⟨hn'.ne', (h Nat.prime_two 0).symm⟩
rsuffices h | h : eval 1 (cyclotomic n ℤ) = 1 ∨ eval 1 (cyclotomic n ℤ) = -1
· have := eval_intCast_map (Int.castRingHom R) (cyclotomic n ℤ) 1
simpa only [map_cyclotomic, Int.cast_one, h, eq_intCast] using this
· exfalso
linarith [cyclotomic_nonneg n (le_refl (1 : ℤ))]
rw [← Int.natAbs_eq_natAbs_iff, Int.natAbs_one, Nat.eq_one_iff_not_exists_prime_dvd]
intro p hp hpe
haveI := Fact.mk hp
have := prod_cyclotomic_eq_geom_sum hn' ℤ
apply_fun eval 1 at this
rw [eval_geom_sum, one_geom_sum, eval_prod, eq_comm, ←
Finset.prod_sdiff <| @range_pow_padicValNat_subset_divisors' p _ _, Finset.prod_image] at this
· simp_rw [eval_one_cyclotomic_prime_pow, Finset.prod_const, Finset.card_range, mul_comm] at this
rw [← Finset.prod_sdiff <| show { n } ⊆ _ from _] at this
swap
· simp only [singleton_subset_iff, mem_sdiff, mem_erase, Ne, mem_divisors, dvd_refl, true_and, mem_image, mem_range,
not_exists, not_and]
exact ⟨⟨hn.ne', hn'.ne'⟩, fun t _ => h hp _⟩
rw [← Int.natAbs_natCast p, Int.natAbs_dvd_natAbs] at hpe
obtain ⟨t, ht⟩ := hpe
rw [Finset.prod_singleton, ht, mul_left_comm, mul_comm, ← mul_assoc, mul_assoc] at this
have : (p : ℤ) ^ padicValNat p n * p ∣ n := ⟨_, this⟩
simp only [← _root_.pow_succ, ← Int.natAbs_dvd_natAbs, Int.natAbs_natCast, Int.natAbs_pow] at this
exact pow_succ_padicValNat_not_dvd hn'.ne' this
· rintro x - y - hxy
apply Nat.succ_injective
exact Nat.pow_right_injective hp.two_le hxy
