OAI/NumberTheory/PowerFree/Model.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.QuarticPowerFree.PowerFree line 11

   Also declared: ComparatorChallenges/PowerFreeValues.lean:12 (same declaration text).

2. def OAI.QuarticPowerFree.rho line 14

   Also declared: ComparatorChallenges/PowerFreeValues.lean:15 (same declaration text).

3. def OAI.QuarticPowerFree.count line 17

   Also declared: ComparatorChallenges/PowerFreeValues.lean:18 (same declaration text).

4. def OAI.QuarticPowerFree.LocallyAdmissible line 21

   Also declared: ComparatorChallenges/PowerFreeValues.lean:22 (same declaration text).

5. def OAI.QuarticPowerFree.localFactor line 24

   Also declared: ComparatorChallenges/PowerFreeValues.lean:25 (same declaration text).

6. def OAI.QuarticPowerFree.densityConstant line 27

   Also declared: ComparatorChallenges/PowerFreeValues.lean:28 (same declaration text).

7. def OAI.QuarticPowerFree.DensityStatement line 30

   Also declared: ComparatorChallenges/PowerFreeValues.lean:31 (same declaration text).