OAI/Combinatorics/BalancedRyser/Incidence/Projective.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Balanced.ProjectiveLine line 9
  2. def OAI.Balanced.ProjectiveIncident line 13
  3. def OAI.Balanced.dualLine line 19
  4. def OAI.Balanced.dualPoint line 24
  5. def OAI.Balanced.affineDualPoint line 29
  6. instance OAI.Balanced.(instance at line 33) line 33
  7. def OAI.Balanced.missedAffine line 39
  8. def OAI.Balanced.missedProjective line 42
  9. def OAI.Balanced.representedDirections line 45
  10. def OAI.Balanced.dualPointSet line 48
  11. def OAI.Balanced.skewProjective line 51