OAI/NumberTheory/EgyptianFractions/Main.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.egyptian_length_is_minimum line 27

   Distinct definitions of this name: ComparatorChallenges/EgyptianFractions.lean:48 (same statement text; different proof or body). Qualify references as OAI.Problem337.egyptian_length_is_minimum@path.

2. theorem OAI.Problem337.main_double_log_order line 40

   Distinct definitions of this name: ComparatorChallenges/EgyptianFractions.lean:57 (same statement text; different proof or body). Qualify references as OAI.Problem337.main_double_log_order@path.

3. theorem OAI.Problem337.one_expansions_finite_and_bounded line 61

   Distinct definitions of this name: ComparatorChallenges/EgyptianFractions.lean:64 (same statement text; different proof or body). Qualify references as OAI.Problem337.one_expansions_finite_and_bounded@path.

4. theorem OAI.Problem337.exact_marker_padding line 73

   Distinct definitions of this name: ComparatorChallenges/EgyptianFractions.lean:78 (same statement text; different proof or body). Qualify references as OAI.Problem337.exact_marker_padding@path.

5. theorem OAI.Problem337.every_exact_marker_occurs line 80

   Distinct definitions of this name: ComparatorChallenges/EgyptianFractions.lean:85 (same statement text; different proof or body). Qualify references as OAI.Problem337.every_exact_marker_occurs@path.

6. theorem OAI.Problem337.quantitative_marked_length line 84

   Distinct definitions of this name: ComparatorChallenges/EgyptianFractions.lean:89 (same statement text; different proof or body). Qualify references as OAI.Problem337.quantitative_marked_length@path.

7. theorem OAI.Problem337.missing_denominator_semantics line 93

   Distinct definitions of this name: ComparatorChallenges/EgyptianFractions.lean:98 (same statement text; different proof or body). Qualify references as OAI.Problem337.missing_denominator_semantics@path.

8. theorem OAI.Problem337.prescribed_denominator_corollary line 103

   Distinct definitions of this name: ComparatorChallenges/EgyptianFractions.lean:107 (same statement text; different proof or body). Qualify references as OAI.Problem337.prescribed_denominator_corollary@path.

9. theorem OAI.Problem337.counting_double_log_order line 120

   Distinct definitions of this name: ComparatorChallenges/EgyptianFractions.lean:71 (same statement text; different proof or body). Qualify references as OAI.Problem337.counting_double_log_order@path.