finite_torsion — Mathlib

English

Let p define the additive circle AddCircle(p). For every n > 0, the set {u in AddCircle(p) | n • u = 0} is finite.

Русский

Пусть p задаёт аддитивный круг AddCircle(p). Для каждого n > 0 множество {u ∈ AddCircle(p) | n · u = 0} конечно.

LaTeX

$$$$ \\{ u \\in \\mathrm{AddCircle}(p) \\mid n \\cdot u = 0 \\} \\text{ finite} $$$$

Lean4

theorem finite_torsion {n : ℕ} (hn : 0 < n) : {u : AddCircle p | n • u = 0}.Finite :=
  by
  convert Set.finite_range (fun m : Fin n ↦ (↑(↑m / ↑n * p) : AddCircle p))
  simp_rw [nsmul_eq_zero_iff hn, range, Fin.exists_iff, exists_prop]

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