OAI/NumberTheory/Ostmann/Construction/InsertedConstituentWords.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Word coordinates for the fixed integer pivot and the retained primes

  1. abbrev OAI.Ostmann.InsertedConstituentVariable line 11
  2. def OAI.Ostmann.insertedConstituentValues line 16
  3. def OAI.Ostmann.insertedConstituentWord line 25
  4. theorem OAI.Ostmann.insertedConstituentWord_prod line 33
  5. theorem OAI.Ostmann.insertedConstituentWord_length_le line 48
  6. def OAI.Ostmann.insertedConstituentPerm line 59
  7. theorem OAI.Ostmann.insertedConstituentValues_perm line 65