OAI/NumberTheory/PiExponent/Cohomology/LocalIntersectionRegularEuler.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PiExponentJets.W28.LocalIntersection.regular_cut_length_ne_top line 13
2. theorem OAI.PiExponentJets.W28.LocalIntersection.regular_colon_length_ne_top line 19
3. theorem OAI.PiExponentJets.W28.LocalIntersection.regular_colon_bot line 26
4. theorem OAI.PiExponentJets.W28.LocalIntersection.cutEuler_bot_regular line 33
5. theorem OAI.PiExponentJets.W28.LocalIntersection.cutEuler_prime_regular line 47
6. theorem OAI.PiExponentJets.W28.LocalIntersection.exists_regular_onecut_sum_and_local_counts line 59