English
If n > 2 and x > 1 in an ordered ring R, then eval x cyclotomic(n, R) > 0.
Русский
Если n > 2 и x > 1 в упорядоченном кольце R, то eval_x циклотомический(n, R) положителен.
LaTeX
$$0 < eval(x, cyclotomic(n, R))$$
Lean4
theorem cyclotomic_pos {n : ℕ} (hn : 2 < n) {R} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (x : R) :
0 < eval x (cyclotomic n R) :=
by
induction n using Nat.strong_induction_on with
| _ n ih
have hn' : 0 < n := pos_of_gt hn
have hn'' : 1 < n := one_lt_two.trans hn
have := prod_cyclotomic_eq_geom_sum hn' R
apply_fun eval x at this
rw [← cons_self_properDivisors hn'.ne', Finset.erase_cons_of_ne _ hn''.ne', Finset.prod_cons, eval_mul,
eval_geom_sum] at this
rcases lt_trichotomy 0 (∑ i ∈ Finset.range n, x ^ i) with (h | h | h)
· apply pos_of_mul_pos_left
· rwa [this]
rw [eval_prod]
refine Finset.prod_nonneg fun i hi => ?_
simp only [Finset.mem_erase, mem_properDivisors] at hi
rw [geom_sum_pos_iff hn'.ne'] at h
rcases h with hk | hx
· refine (ih _ hi.2.2 (Nat.two_lt_of_ne ?_ hi.1 ?_)).le <;> rintro rfl
· exact hn'.ne' (zero_dvd_iff.mp hi.2.1)
· exact not_odd_iff_even.2 (even_iff_two_dvd.mpr hi.2.1) hk
· rcases eq_or_ne i 2 with (rfl | hk)
· simpa only [eval_X, eval_one, cyclotomic_two, eval_add] using hx.le
refine (ih _ hi.2.2 (Nat.two_lt_of_ne ?_ hi.1 hk)).le
rintro rfl
exact hn'.ne' <| zero_dvd_iff.mp hi.2.1
· rw [eq_comm, geom_sum_eq_zero_iff_neg_one hn'.ne'] at h
exact h.1.symm ▸ cyclotomic_neg_one_pos hn
· apply pos_of_mul_neg_left
· rwa [this]
rw [geom_sum_neg_iff hn'.ne'] at h
have h2 : 2 ∈ n.properDivisors.erase 1 :=
by
rw [Finset.mem_erase, mem_properDivisors]
exact ⟨by decide, even_iff_two_dvd.mp h.1, hn⟩
rw [eval_prod, ← Finset.prod_erase_mul _ _ h2]
apply mul_nonpos_of_nonneg_of_nonpos
· refine Finset.prod_nonneg fun i hi => le_of_lt ?_
simp only [Finset.mem_erase, mem_properDivisors] at hi
refine ih _ hi.2.2.2 (Nat.two_lt_of_ne ?_ hi.2.1 hi.1)
rintro rfl
rw [zero_dvd_iff] at hi
exact hn'.ne' hi.2.2.1
· simpa only [eval_X, eval_one, cyclotomic_two, eval_add] using h.right.le
