Module

NumberFieldPowerDivisibility.lean

Nyll.AnabelianGeometry.KummerTheory.NumberFieldPowerDivisibility

1 declaration indexed from sourceView source ↗

Module documentation

A uniform divisibility bound for powers of a number-field element

For a fixed non-torsion element a, one positive integer M controls all relations a^e = d^n in the original number field: n divides eM. A fixed S-unit group contains both a and every possible d in these relations.

Imports2

Imported by1

Nyll.AnabelianGeometry.KummerTheory.All

theorem

exists_power_divisibility_bound

L26 ↗

AnabelianGeometry.KummerTheory.exists_power_divisibility_bound

Documentation

Powers of one non-torsion number-field element have uniformly bounded denominators. The witnesses to all power relations are allowed to vary.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace AnabelianGeometry.KummerTheory
variable {K : Type*} [Field K] [NumberField K]

Lean source · statement

theorem exists_power_divisibility_bound (a : Kˣ) (ha : ¬ IsOfFinOrder a) :
    ∃ M : ℕ+, ∀ (e : ℤ) (n : ℕ+) (d : Kˣ),
      a ^ e = d ^ (n : ℕ) → (n : ℤ) ∣ e * (M : ℤ)

Module documentation

A uniform divisibility bound for powers of a number-field element

Declarations

exists_power_divisibility_bound