OAI/Probability/CriticalPercolation/LinearGroups/ProjectivelyPeriodicSchur.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.LinearGrowth.linearMatrixEquiv line 15
2. lemma OAI.CriticalPercolation.LinearGrowth.finite_range_of_torsion_linearEquiv line 19
3. def OAI.CriticalPercolation.LinearGrowth.conjugationRepresentation line 35
4. lemma OAI.CriticalPercolation.LinearGrowth.conjugation_eq_one_of_scalar line 41
5. lemma OAI.CriticalPercolation.LinearGrowth.exists_finiteIndex_comm_range_of_projectively_periodic line 48