OAI/Probability/CriticalPercolation/Nilpotent/CharacteristicNilpotentCore.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalPercolation.SparseGrowth.HasPolynomialDegree.of_surjective line 14
2. def OAI.CriticalPercolation.SparseGrowth.powerSubgroup line 30
3. instance OAI.CriticalPercolation.SparseGrowth.powerSubgroup_characteristic line 34
4. lemma OAI.CriticalPercolation.SparseGrowth.powerSubgroup_le_finiteIndex line 43
5. lemma OAI.CriticalPercolation.SparseGrowth.powerSubgroup_finiteIndex_of_solvable_growth line 55
6. theorem OAI.CriticalPercolation.SparseGrowth.HasPolynomialDegree.characteristic_nilpotent_core line 72
7. lemma OAI.CriticalPercolation.SparseGrowth.characteristic_map_normal line 92