OAI/Combinatorics/BalancedRyser/Incidence/Affine.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Balanced.Point line 10
  2. abbrev OAI.Balanced.Direction line 11
  3. abbrev OAI.Balanced.Line line 12
  4. abbrev OAI.Balanced.ProjectivePoint line 13
  5. def OAI.Balanced.lineEval line 17
  6. def OAI.Balanced.OnLine line 21
  7. def OAI.Balanced.lineThrough line 23
  8. def OAI.Balanced.ThroughProjective line 25
  9. def OAI.Balanced.joiningLine line 29
  10. def OAI.Balanced.lineIntersection line 34
  11. instance OAI.Balanced.(instance at line 45) line 45
  12. instance OAI.Balanced.(instance at line 48) line 48
  13. def OAI.Balanced.linePoints line 53
  14. def OAI.Balanced.linesInDirection line 55
  15. def OAI.Balanced.CoversPoints line 58