OAI/Probability/CriticalPercolation/LinearGroups/CongruenceTorsion.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalPercolation.LinearGrowth.one_add_pow_of_sq_zero line 14
2. lemma OAI.CriticalPercolation.LinearGrowth.scalar_inverse_mod line 23
3. lemma OAI.CriticalPercolation.LinearGrowth.congruence_power_step line 31
4. lemma OAI.CriticalPercolation.LinearGrowth.eq_one_of_prime_to_residue_order line 67
5. lemma OAI.CriticalPercolation.LinearGrowth.int_isJacobsonRing line 84
6. lemma OAI.CriticalPercolation.LinearGrowth.finite_field_of_finiteType_int line 99
7. lemma OAI.CriticalPercolation.LinearGrowth.finite_residue_of_finiteType_int line 115
8. lemma OAI.CriticalPercolation.LinearGrowth.exists_maximal_avoiding line 121