OAI/Probability/CriticalPercolation/Growth/CosetFiniteCore.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalPercolation.RelativeGrowth.conjugate_map_one line 15
2. lemma OAI.CriticalPercolation.RelativeGrowth.conjugate_eq_of_normalizer line 17
3. lemma OAI.CriticalPercolation.RelativeGrowth.conjugate_stabilizer_relIndex line 24
4. lemma OAI.CriticalPercolation.RelativeGrowth.conjugate_commensurable_index line 33
5. lemma OAI.CriticalPercolation.RelativeGrowth.finite_conjugate_family_of_finiteIndex_normalizer line 42
6. lemma OAI.CriticalPercolation.RelativeGrowth.HasDegree.finiteIndex_normal_core line 55