Registry · Proposition III.P25 tau-effective formalized

III.P25 — Mordell-Weil Analogue

Group of τ-rational points is finitely generated at each primorial level; rank stabilizes at finite depth

Book III Part 6 Ch. 45

Dependency Graph

Depends on (2)

III.D59 III.D60

Depended on by (2)

III.P26 III.T35

Lean Formalization

Module: TauLib.BookIII.Arithmetic.RationalPoints

Symbol: mordell_weil_check