OAI/GroupTheory/FiniteIndex/Extension.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Finite generation of a group extension with finitely generated kernel and quotient.

  1. lemma OAI.FiniteIndexRealization.fg_of_surjective_with_fg_kernel line 8