even_torsionOrder — Mathlib

English

The order of the torsion subgroup is even.

Русский

Порядок торсионной подгруппы чётен.

LaTeX

$$$\mathrm{Even}(\mathrm{torsionOrder}(K))$$$

Lean4

theorem even_torsionOrder : Even (torsionOrder K) :=
  by
  suffices orderOf (⟨-1, neg_one_mem_torsion⟩ : torsion K) = 2
    by
    rw [even_iff_two_dvd, ← this]
    exact orderOf_dvd_card
  rw [← Subgroup.orderOf_coe, ← orderOf_units, Units.val_neg, val_one, orderOf_neg_one, ringChar.eq_zero,
    if_neg (by decide)]

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