OAI/Analysis/IrrationalRotation/Model/MixedRadix.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Invariant233.MixedRadix.denominator line 9
  2. abbrev OAI.Invariant233.MixedRadix.Digits line 12
  3. def OAI.Invariant233.MixedRadix.term line 14
  4. def OAI.Invariant233.MixedRadix.ofDigits line 17
  5. def OAI.Invariant233.MixedRadix.tailValue line 20
  6. def OAI.Invariant233.MixedRadix.prefixRank line 23
  7. def OAI.Invariant233.MixedRadix.Nonterminal line 27
  8. def OAI.Invariant233.MixedRadix.canonicalDigits line 30
  9. def OAI.Invariant233.MixedRadix.extendPrefix line 33
  10. def OAI.Invariant233.MixedRadix.radices line 37
  11. def OAI.Invariant233.MixedRadix.hybrid line 39