OAI/Analysis/PlanarPacking/HexLattice.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpPlanar.hexPoint line 7
  2. def OAI.SharpPlanar.hexForm line 9
  3. def OAI.SharpPlanar.hexNat line 10
  4. lemma OAI.SharpPlanar.hexForm_nonneg line 11
  5. lemma OAI.SharpPlanar.hexForm_zero_iff line 14
  6. lemma OAI.SharpPlanar.hexNat_coe line 24
  7. lemma OAI.SharpPlanar.hexNat_zero_iff line 25
  8. lemma OAI.SharpPlanar.hexNat_pos line 29
  9. lemma OAI.SharpPlanar.hexResidue_table line 30
  10. lemma OAI.SharpPlanar.hexNat_residue line 32
  11. def OAI.SharpPlanar.hexNode line 45
  12. lemma OAI.SharpPlanar.hexPoint_radius line 46
  13. def OAI.SharpPlanar.firstShell line 57
  14. lemma OAI.SharpPlanar.firstShell_card line 58
  15. lemma OAI.SharpPlanar.firstShell_iff line 59