English
The second modified cyclotomic polynomial is X + 1 when the characteristic is not 2.
Русский
Вторая модифицированная циклотомическая равна X + 1, если характеристика не равна 2.
LaTeX
$$$\text{cyclotomic}'(2, R) = X + 1$$$
Lean4
/-- The second modified cyclotomic polynomial is `X + 1` if the characteristic of `R` is not `2`. -/
-- Cannot be @[simp] because `p` cannot be inferred by `simp`.
theorem cyclotomic'_two (R : Type*) [CommRing R] [IsDomain R] (p : ℕ) [CharP R p] (hp : p ≠ 2) :
cyclotomic' 2 R = X + 1 := by
rw [cyclotomic']
have prim_root_two : primitiveRoots 2 R = {(-1 : R)} :=
by
simp only [Finset.eq_singleton_iff_unique_mem, mem_primitiveRoots two_pos]
exact ⟨IsPrimitiveRoot.neg_one p hp, fun x => IsPrimitiveRoot.eq_neg_one_of_two_right⟩
simp only [prim_root_two, Finset.prod_singleton, RingHom.map_neg, RingHom.map_one, sub_neg_eq_add]
