OAI/Probability/CriticalPercolation/LinearGroups/AllPlaceKronecker.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalPercolation.Arithmetic.algebraic_of_all_complex_embeddings_bounded line 14
2. lemma OAI.CriticalPercolation.Arithmetic.uncountable_padic_closure line 20
3. lemma OAI.CriticalPercolation.Arithmetic.root_of_unity_of_all_places line 25