OAI/GroupTheory/FiniteKernel/VirtualAbelian.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Campana.VirtuallyAbelian line 10
2. theorem OAI.Campana.commutatorSet_subset_ker line 18
3. theorem OAI.Campana.finiteIndex_center_of_finite_kernel line 27
4. theorem OAI.Campana.virtuallyAbelian_of_finite_kernel line 36
5. theorem OAI.Campana.finiteIndex_map_subtype line 48
6. theorem OAI.Campana.virtuallyAbelian_of_finiteIndex line 54
7. theorem OAI.Campana.virtuallyAbelian_of_surjective line 65
8. theorem OAI.Campana.virtuallyAbelian_iff_mulEquiv line 78
9. theorem OAI.Campana.virtuallyAbelian_fundamentalGroup_iff line 87
10. theorem OAI.Campana.residuallyFinite_of_injective line 97
11. theorem OAI.Campana.residuallyFinite_pi line 109
12. theorem OAI.Campana.residuallyFinite_int line 119
13. theorem OAI.Campana.residuallyFinite_of_fg_commGroup line 135
14. theorem OAI.Campana.residuallyFinite_of_finiteIndex line 148
15. theorem OAI.Campana.residuallyFinite_of_fg_virtuallyAbelian line 165
16. theorem OAI.Campana.exists_finiteIndex_disjoint line 175
17. theorem OAI.Campana.finite_by_abelian line 197