Theorem CommGroup.fg_of_descent

Modification history

2026-03-02 16:30

Mathlib/GroupTheory/Descent.lean

feat(GroupTheory/Descent): add abstract descent theorem (#35918) …

Added CommGroup.fg_of_descent View on Github →