English
For any x in the ring of integers, λ divides x, or x−1, or x+1.
Русский
Для любого x в кольце целых λ делит x, или x−1, или x+1.
LaTeX
$$$\lambda \mid x \quad \text{или} \quad \lambda \mid (x-1) \quad \text{или} \quad \lambda \mid (x+1)$$$
Lean4
/-- If a unit `u` is congruent to an integer modulo `λ ^ 2`, then `u = 1` or `u = -1`.
This is a special case of the so-called *Kummer's lemma*. -/
theorem eq_one_or_neg_one_of_unit_of_congruent [NumberField K] [IsCyclotomicExtension { 3 } ℚ K]
(hcong : ∃ n : ℤ, λ ^ 2 ∣ (u - n : 𝓞 K)) : u = 1 ∨ u = -1 :=
by
replace hcong : ∃ n : ℤ, (3 : 𝓞 K) ∣ (↑u - n : 𝓞 K) :=
by
obtain ⟨n, x, hx⟩ := hcong
exact ⟨n, -η * x, by rw [← mul_assoc, mul_neg, ← neg_mul, ← lambda_sq, hx]⟩
have hζ := IsCyclotomicExtension.zeta_spec 3 ℚ K
have := Units.mem hζ u
fin_cases this
· left; rfl
· right; rfl
all_goals exfalso
· exact hζ.not_exists_int_prime_dvd_sub_of_prime_ne_two' (by decide) hcong
· apply hζ.not_exists_int_prime_dvd_sub_of_prime_ne_two' (by decide)
obtain ⟨n, x, hx⟩ := hcong
rw [sub_eq_iff_eq_add] at hx
refine ⟨-n, -x, sub_eq_iff_eq_add.2 ?_⟩
simp only [Nat.cast_ofNat, mul_neg, Int.cast_neg, ← neg_add, ← hx, Units.val_neg, IsUnit.unit_spec,
RingOfIntegers.neg_mk, neg_neg]
· exact (hζ.pow_of_coprime 2 (by decide)).not_exists_int_prime_dvd_sub_of_prime_ne_two' (by decide) hcong
· apply (hζ.pow_of_coprime 2 (by decide)).not_exists_int_prime_dvd_sub_of_prime_ne_two' (by decide)
obtain ⟨n, x, hx⟩ := hcong
refine ⟨-n, -x, sub_eq_iff_eq_add.2 ?_⟩
have : (hζ.pow_of_coprime 2 (by decide)).toInteger = hζ.toInteger ^ 2 := by ext; simp
simp only [this, Nat.cast_ofNat, mul_neg, Int.cast_neg, ← neg_add, ← sub_eq_iff_eq_add.1 hx, Units.val_neg,
val_pow_eq_pow_val, IsUnit.unit_spec, neg_neg]
