torsionOrder_eq_two_of_odd_finrank

English

If the rational finrank of K is odd, then torsionOrder(K) = 2.

Русский

При нечётной финразмерности torsionOrder(K) = 2.

LaTeX

$$$\mathrm{torsionOrder}(K) = 2$$$

Lean4

theorem torsionOrder_eq_two_of_odd_finrank (h : Odd (Module.finrank ℚ K)) : torsionOrder K = 2 := by
  classical
  refine
    (Finset.card_eq_two.2
      ⟨1, ⟨-1, neg_one_mem_torsion⟩, by simp [← Subtype.coe_ne_coe],
        Finset.ext fun x ↦ ⟨fun _ ↦ ?_, fun _ ↦ Finset.mem_univ _⟩⟩)
  rw [Finset.mem_insert, Finset.mem_singleton, ← Subtype.val_inj, ← Subtype.val_inj]
  exact torsion_eq_one_or_neg_one_of_odd_finrank h x

Похожие утверждения