OAI/NumberTheory/Ostmann/Arithmetic/LogCellPartitionMesh.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Ostmann.Arithmetic.LogCellPartition.boxLower_le_boxUpper line 12
  2. theorem OAI.Ostmann.Arithmetic.LogCellPartition.boxLower_mem_interval line 17
  3. theorem OAI.Ostmann.Arithmetic.LogCellPartition.boxUpper_mem_interval line 22
  4. theorem OAI.Ostmann.Arithmetic.LogCellPartition.box_width_le line 27

    Distinct definitions of this name: OAI/NumberTheory/Ostmann/Arithmetic/PrimeCellGridIdentities.lean:38 (different declaration text). Qualify references as OAI.Ostmann.Arithmetic.LogCellPartition.box_width_le@path.

  5. theorem OAI.Ostmann.Arithmetic.LogCellPartition.gridCount_le_meshIntervals line 32
  6. theorem OAI.Ostmann.Arithmetic.LogCellPartition.gridBoxIndex_card line 37
  7. theorem OAI.Ostmann.Arithmetic.LogCellPartition.gridBoxIndex_card_le_mesh_power line 42