OAI/Probability/CriticalPercolation/LinearGroups/FullSpanAlternative.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.LinearGrowth.FullSpan line 15
2. def OAI.CriticalPercolation.LinearGrowth.StrongFullSpan line 18
3. lemma OAI.CriticalPercolation.LinearGrowth.submodule_eq_bot_or_top_of_fullSpan line 21
4. lemma OAI.CriticalPercolation.LinearGrowth.no_finite_subspace_orbit_of_strongFullSpan line 44
5. def OAI.CriticalPercolation.LinearGrowth.continuousRepresentation line 56
6. lemma OAI.CriticalPercolation.LinearGrowth.projective_bound_of_strongFullSpan line 61