OAI/NumberTheory/Ostmann/Supply/TruncatedBilinearCube.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact truncation of the two subset choices

  1. theorem OAI.Ostmann.cubeCoefficient_truncation line 10
  2. def OAI.Ostmann.subsetPairFactor line 36
  3. theorem OAI.Ostmann.subsetPair_cubeCoefficient line 42
  4. theorem OAI.Ostmann.elementaryTruncation_square_cube line 54