English
For k < n, there exists z with z ∈ adjoin ℤ { μ } such that n = z * (μ - 1)^k, when μ is a primitive (n+1)-th root of unity.
Русский
Для k < n, существует z ∈ adjoin ℤ { μ }, такое что n = z*(μ-1)^k, когда μ — примитивный (n+1)-й корень единицы.
LaTeX
$$∃ z ∈ adjoin ℤ { μ }, n = z * (μ - 1)^k$$
Lean4
/-- If `μ` is a primitive `n`th root of unity in `R` and `k < n`, then `n` is divisible
by `(μ-1)^k` in `ℤ[μ] ⊆ R`. -/
theorem self_sub_one_pow_dvd_order {k n : ℕ} (hn : k < n) {μ : R} (hμ : IsPrimitiveRoot μ n) :
∃ z ∈ adjoin ℤ { μ }, n = z * (μ - 1) ^ k := by
let n' + 1 := n
obtain ⟨m, rfl⟩ := Nat.exists_eq_add_of_le' (Nat.le_of_lt_succ hn)
have hdvd k : ∃ z ∈ adjoin ℤ { μ }, μ ^ k - 1 = z * (μ - 1) :=
by
refine ⟨(Finset.range k).sum (μ ^ ·), ?_, (geom_sum_mul μ k).symm⟩
exact Subalgebra.sum_mem _ fun m _ ↦ Subalgebra.pow_mem _ (self_mem_adjoin_singleton _ μ) _
let Z k := Classical.choose <| hdvd k
have Zdef k : Z k ∈ adjoin ℤ { μ } ∧ μ ^ k - 1 = Z k * (μ - 1) := Classical.choose_spec <| hdvd k
refine ⟨(-1) ^ (m + k) * (∏ j ∈ range k, Z (j + 1)) * ∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1), ?_, ?_⟩
· apply Subalgebra.mul_mem
· apply Subalgebra.mul_mem
· exact Subalgebra.pow_mem _ (Subalgebra.neg_mem _ <| Subalgebra.one_mem _) _
· exact Subalgebra.prod_mem _ fun _ _ ↦ (Zdef _).1
· refine Subalgebra.prod_mem _ fun _ _ ↦ ?_
apply Subalgebra.sub_mem
· exact Subalgebra.pow_mem _ (self_mem_adjoin_singleton ℤ μ) _
· exact Subalgebra.one_mem _
· push_cast
have := Nat.cast_add (R := R) m k ▸ hμ.prod_pow_sub_one_eq_order
rw [← this, mul_assoc, mul_assoc]
congr 1
conv => enter [2, 2, 2]; rw [← card_range k]
rw [← prod_range_mul_prod_Ico _ (Nat.le_add_left k m), mul_comm _ (_ ^ #_), ← mul_assoc, prod_mul_pow_card]
conv => enter [2, 1, 2, j]; rw [← (Zdef _).2]
