OAI/Combinatorics/SquareDifference/SmallRoots.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SquareDifference.smallStrict line 15
2. lemma OAI.SquareDifference.exists_small_root line 18
3. def OAI.SquareDifference.smallModulus line 44
4. lemma OAI.SquareDifference.smallModulus_dvd line 46
5. def OAI.SquareDifference.smallProjection line 51
6. lemma OAI.SquareDifference.smallProjection_nat line 54
7. def OAI.SquareDifference.smallStrictPair line 56