Theorems · Theorem · group theory

CommGroup.finite_torsion_of_descent

∀ {G : Type u_1} [inst : CommGroup G] {n : ℕ} {h : G → ℝ} {b c₀ : ℝ},
  1 < b → (∀ (x : G), b * h x - c₀ ≤ h (x ^ n)) → ∀ [Northcott h], Finite ↥(CommGroup.torsion G)

If G is a commutative group and n : ℕ, h : G → ℝ satisfy * for all x : G, h (x ^ n) ≥ b * h x - c₀, * for all B : ℝ, there are only finitely many x : G such that h x ≤ B, where 1 < b and c₀ are real numbers, then the torsion subgroup of G is finite.

Defined in

Mathlib.GroupTheory.Descent

Cited by

1 results in Mathlib

Foundations

Depth 118 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommGroupNorthcott