Commit 2026-03-02 16:30 1477c66e
View on Github →feat(GroupTheory/Descent): add abstract descent theorem (#35918) This PR adds three consecutively more specialized versions of the "descent theorem", which says that if a group is equipped with a height function satisfying certain axioms, then the group is finitely-generated. The final version is the form suitable to be used in a proof of the Mordell-Weil Theorem.