OAI/Combinatorics/SquareDifference/PrimeExtension.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SquareDifference.extendedPrime line 20
2. def OAI.SquareDifference.extendedRoots line 22
3. lemma OAI.SquareDifference.inl_mem_extendedRoots line 24
4. lemma OAI.SquareDifference.inr_mem_extendedRoots line 30
5. def OAI.SquareDifference.outsideSumEquiv line 36
6. lemma OAI.SquareDifference.extendedPrime_injective line 48
7. instance OAI.SquareDifference.extendedPrime_prime line 64
8. lemma OAI.SquareDifference.extended_roots_modulus line 67
9. lemma OAI.SquareDifference.extended_outside_modulus line 82
10. lemma OAI.SquareDifference.primary_product_cover line 93