English
If a unit u in the ring of integers is congruent modulo λ^2 to an integer, then u equals 1 or -1.
Русский
Если единица u в кольце целых по модулю λ^2 конгруентна целому числу, то u равно 1 или -1.
LaTeX
$$$\exists n \in \mathbb{Z}, \ λ^2 \mid (u - n) \Rightarrow (u = 1 \lor u = -1)$$$
Lean4
/-- Let `(x : 𝓞 K)`. Then we have that `λ` divides one amongst `x`, `x - 1` and `x + 1`. -/
theorem lambda_dvd_or_dvd_sub_one_or_dvd_add_one [NumberField K] [IsCyclotomicExtension { 3 } ℚ K] :
λ ∣ x ∨ λ ∣ x - 1 ∨ λ ∣ x + 1 := by
classical
have := hζ.finite_quotient_toInteger_sub_one (by decide)
let _ := Fintype.ofFinite (𝓞 K ⧸ Ideal.span {λ})
let _ : Ring (𝓞 K ⧸ Ideal.span {λ}) := CommRing.toRing
let _ : AddGroup (𝓞 K ⧸ Ideal.span {λ}) := AddGroupWithOne.toAddGroup
have := Finset.mem_univ (Ideal.Quotient.mk (Ideal.span {λ}) x)
have h3 : Fintype.card (𝓞 K ⧸ Ideal.span {λ}) = 3 :=
by
rw [← Nat.card_eq_fintype_card, hζ.card_quotient_toInteger_sub_one,
hζ.norm_toInteger_sub_one_of_prime_ne_two' (by decide)]
simp only [Nat.cast_ofNat, Int.reduceAbs]
rw [Finset.univ_of_card_le_three h3.le] at this
simp only [Finset.mem_insert, Finset.mem_singleton] at this
rcases this with h | h | h
· left
exact Ideal.mem_span_singleton.1 <| Ideal.Quotient.eq_zero_iff_mem.1 h
· right; left
refine Ideal.mem_span_singleton.1 <| Ideal.Quotient.eq_zero_iff_mem.1 ?_
rw [RingHom.map_sub, h, RingHom.map_one, sub_self]
· right; right
refine Ideal.mem_span_singleton.1 <| Ideal.Quotient.eq_zero_iff_mem.1 ?_
rw [RingHom.map_add, h, RingHom.map_one, neg_add_cancel]
