English
Over characteristic zero, the map n -> cyclotomic(n, R) from natural numbers to polynomials is injective.
Русский
В характеристике ноль отображение n ↦ cyclotomic(n, R) инъективно.
LaTeX
$$$$ \\text{cyclotomic}: \\mathbb{N} \\to \\{\\text{polynomials over } R\\} \\text{ is injective}. $$$$
Lean4
/-- Over a ring `R` of characteristic zero, `fun n => cyclotomic n R` is injective. -/
theorem cyclotomic_injective [CharZero R] : Function.Injective fun n => cyclotomic n R :=
by
intro n m hnm
simp only at hnm
rcases eq_or_ne n 0 with (rfl | hzero)
· rw [cyclotomic_zero] at hnm
replace hnm := congr_arg natDegree hnm
rwa [natDegree_one, natDegree_cyclotomic, eq_comm, Nat.totient_eq_zero, eq_comm] at hnm
· haveI := NeZero.mk hzero
rw [← map_cyclotomic_int _ R, ← map_cyclotomic_int _ R] at hnm
replace hnm := map_injective (Int.castRingHom R) Int.cast_injective hnm
replace hnm := congr_arg (map (Int.castRingHom ℂ)) hnm
rw [map_cyclotomic_int, map_cyclotomic_int] at hnm
have hprim := Complex.isPrimitiveRoot_exp _ hzero
have hroot := isRoot_cyclotomic_iff (R := ℂ).2 hprim
rw [hnm] at hroot
haveI hmzero : NeZero m := ⟨fun h => by simp [h] at hroot⟩
rw [isRoot_cyclotomic_iff (R := ℂ)] at hroot
replace hprim := hprim.eq_orderOf
rwa [← IsPrimitiveRoot.eq_orderOf hroot] at hprim
