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 →