English
If the rational finrank of K is odd, every torsion unit in 𝓞_K is either 1 or -1.
Русский
Если нечётна размерность K над ℚ, то любая торсионная единица в 𝓞_K равна либо 1, либо -1.
LaTeX
$$$\text{Odd}(\operatorname{Module.finrank} \mathbb{Q} K) \Rightarrow \forall x \in \mathrm{torsion}(K),\; x = 1 \text{ или } x = -1$$$
Lean4
theorem torsion_eq_one_or_neg_one_of_odd_finrank (h : Odd (Module.finrank ℚ K)) (x : torsion K) :
(x : (𝓞 K)ˣ) = 1 ∨ (x : (𝓞 K)ˣ) = -1 :=
by
by_cases hc : 2 < orderOf (x : (𝓞 K)ˣ)
· rw [← orderOf_units, ← orderOf_submonoid] at hc
linarith [IsPrimitiveRoot.nrRealPlaces_eq_zero_of_two_lt hc (IsPrimitiveRoot.orderOf (x.1 : K)),
NumberField.InfinitePlace.nrRealPlaces_pos_of_odd_finrank h]
· push_neg at hc
interval_cases hi : orderOf (x : (𝓞 K)ˣ)
· linarith [orderOf_pos_iff.2 ((CommGroup.mem_torsion _ x.1).1 x.2)]
· exact Or.intro_left _ (orderOf_eq_one_iff.1 hi)
· rw [← orderOf_units, CharP.orderOf_eq_two_iff 0 (by decide)] at hi
simp [← Units.val_inj, ← Units.val_inj, Units.val_neg, Units.val_one, hi]
