OAI/NumberTheory/ShortEgyptian/DescentSets.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ShortEgyptian.HasUnitSum line 12
2. lemma OAI.ShortEgyptian.HasUnitSum.mono line 15
3. lemma OAI.ShortEgyptian.hasUnitSum_zero line 19
4. lemma OAI.ShortEgyptian.HasUnitSum.scale line 22
5. def OAI.ShortEgyptian.levelBad line 41
6. lemma OAI.ShortEgyptian.mem_levelBad line 44
7. lemma OAI.ShortEgyptian.levelBad_card_le line 55
8. lemma OAI.ShortEgyptian.level_fraction_lt line 62
9. lemma OAI.ShortEgyptian.levelBad_terminal line 81
10. lemma OAI.ShortEgyptian.levelBad_inherit line 93
11. lemma OAI.ShortEgyptian.levelBad_residue line 104