OAI/Combinatorics/SquareDifference/Main.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SquareDifference.density_root_bound line 11
  2. lemma OAI.SquareDifference.nat_power_saving line 21
  3. def OAI.SquareDifference.natTranslate line 54
  4. lemma OAI.SquareDifference.natTranslate_sub line 56
  5. lemma OAI.SquareDifference.natTranslate_card line 63
  6. lemma OAI.SquareDifference.natTranslate_free line 71
  7. theorem OAI.SquareDifference.power_saving line 83

    Distinct definitions of this name: ComparatorChallenges/SquareDifference.lean:10 (different declaration text). Qualify references as OAI.SquareDifference.power_saving@path.