OAI/Probability/CriticalPercolation/LinearGroups/InvariantBlockSolvability.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.LinearGrowth.subspaceRepresentation line 12
2. def OAI.CriticalPercolation.LinearGrowth.quotientRepresentation line 18
3. lemma OAI.CriticalPercolation.LinearGrowth.subspaceRepresentation_apply line 30
4. lemma OAI.CriticalPercolation.LinearGrowth.quotientRepresentation_apply line 34
5. lemma OAI.CriticalPercolation.LinearGrowth.commute_of_identity_on_subspace_quotient line 38
6. lemma OAI.CriticalPercolation.LinearGrowth.solvable_of_subspace_quotient line 51