English
If a cyclotomic extension over ℚ contains a primitive l-th root of unity, and l ≠ 0, then l divides 2n.
Русский
Если циклотомическое расширение над ℚ содержит примитивный l-юдов корень единицы и l ≠ 0, то l делится на 2n.
LaTeX
$$$$ l \mid 2n $$$$
Lean4
/-- If a `n`-th cyclotomic extension of `ℚ` contains a primitive `l`-th root of unity, then
`l ∣ 2 * n`. -/
theorem dvd_of_isCyclotomicExtension [IsCyclotomicExtension { n } ℚ K] {ζ : K} {l : ℕ} (hζ : IsPrimitiveRoot ζ l)
(hl : l ≠ 0) : l ∣ 2 * n := by
have hl : NeZero l := ⟨hl⟩
have hroot := IsCyclotomicExtension.zeta_spec n ℚ K
have key :=
IsPrimitiveRoot.lcm_totient_le_finrank hζ hroot
(cyclotomic.irreducible_rat <| Nat.lcm_pos (Nat.pos_of_ne_zero hl.1) (NeZero.pos n))
rw [IsCyclotomicExtension.finrank K (cyclotomic.irreducible_rat (NeZero.pos n))] at key
rcases _root_.dvd_lcm_right l n with ⟨r, hr⟩
have ineq := Nat.totient_super_multiplicative n r
rw [← hr] at ineq
replace key := (mul_le_iff_le_one_right (Nat.totient_pos.2 (NeZero.pos n))).mp (le_trans ineq key)
have rpos : 0 < r := by
refine Nat.pos_of_ne_zero (fun h ↦ ?_)
simp only [h, mul_zero, _root_.lcm_eq_zero_iff, NeZero.ne _, or_false] at hr
replace key := (Nat.dvd_prime Nat.prime_two).1 (Nat.dvd_two_of_totient_le_one rpos key)
rcases key with (key | key)
· rw [key, mul_one] at hr
rw [← hr]
exact dvd_mul_of_dvd_right (_root_.dvd_lcm_left l n) 2
· rw [key, mul_comm] at hr
simpa [← hr] using _root_.dvd_lcm_left _ _
