OAI/Probability/CriticalPercolation/LinearGroups/SolvableGrowth.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalPercolation.SparseGrowth.isMulCommutative_of_generators line 15
2. lemma OAI.CriticalPercolation.SparseGrowth.commutator_eq_normalClosure_generators line 25
3. theorem OAI.CriticalPercolation.SparseGrowth.HasPolynomialDegree.commutator_fg line 49
4. lemma OAI.CriticalPercolation.SparseGrowth.subgroup_fg_map line 56
5. theorem OAI.CriticalPercolation.SparseGrowth.HasPolynomialDegree.derivedSeries_fg line 62
6. lemma OAI.CriticalPercolation.SparseGrowth.finite_of_fg_torsion_finite_commutator line 75
7. lemma OAI.CriticalPercolation.SparseGrowth.map_derivedSeries_commutator line 85
8. theorem OAI.CriticalPercolation.SparseGrowth.finite_of_torsion_derivedSeries_eq_bot line 97
9. theorem OAI.CriticalPercolation.SparseGrowth.finite_of_torsion_solvable_sparse_growth line 128