OAI/NumberTheory/Ostmann/Tree/QuartetFactorizationFrames.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Ostmann.Tree.QuartetFactorization.Frame line 12
  2. def OAI.Ostmann.Tree.QuartetFactorization.Frame.value line 20
  3. def OAI.Ostmann.Tree.QuartetFactorization.Frame.argument line 23
  4. def OAI.Ostmann.Tree.QuartetFactorization.propagate line 28
  5. theorem OAI.Ostmann.Tree.QuartetFactorization.propagate_project_split line 40
  6. def OAI.Ostmann.Tree.QuartetFactorization.frameProduct line 52
  7. theorem OAI.Ostmann.Tree.QuartetFactorization.frameProduct_join line 58
  8. theorem OAI.Ostmann.Tree.QuartetFactorization.evaluate_incoming_irrelevant line 67
  9. theorem OAI.Ostmann.Tree.QuartetFactorization.evaluate_factorization line 73