OAI/Combinatorics/BalancedRyser/Incidence/ProjectiveNormalization.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Balanced.ProjectiveNormalization.V line 13
  2. structure OAI.Balanced.ProjectiveNormalization.Collineation line 15
  3. def OAI.Balanced.ProjectiveNormalization.pointEquiv line 20
  4. def OAI.Balanced.ProjectiveNormalization.normalizeLine line 41
  5. theorem OAI.Balanced.ProjectiveNormalization.normalize_homogeneousLine line 46
  6. theorem OAI.Balanced.ProjectiveNormalization.normalizeLine_smul line 54
  7. theorem OAI.Balanced.ProjectiveNormalization.exists_smul_homogeneousLine line 60
  8. def OAI.Balanced.ProjectiveNormalization.lineEquiv line 85
  9. def OAI.Balanced.ProjectiveNormalization.ofLinear line 106
  10. def OAI.Balanced.ProjectiveNormalization.Collineation.refl line 132
  11. def OAI.Balanced.ProjectiveNormalization.Collineation.trans line 137
  12. def OAI.Balanced.ProjectiveNormalization.Collineation.symm line 142
  13. def OAI.Balanced.ProjectiveNormalization.coordAdd line 149
  14. def OAI.Balanced.ProjectiveNormalization.addCoordinate line 175
  15. def OAI.Balanced.ProjectiveNormalization.coordPerm line 181
  16. theorem OAI.Balanced.ProjectiveNormalization.coordPerm_apply line 189
  17. def OAI.Balanced.ProjectiveNormalization.permuteCoordinates line 192
  18. def OAI.Balanced.ProjectiveNormalization.pointToInfinity line 197
  19. theorem OAI.Balanced.ProjectiveNormalization.pointToInfinity_apply line 208
  20. def OAI.Balanced.ProjectiveNormalization.verticalToInfinity line 221
  21. theorem OAI.Balanced.ProjectiveNormalization.verticalToInfinity_point line 225
  22. theorem OAI.Balanced.ProjectiveNormalization.verticalToInfinity_line line 231
  23. theorem OAI.Balanced.ProjectiveNormalization.exists_flag_normalization line 237
  24. theorem OAI.Balanced.ProjectiveNormalization.card_image line 263
  25. theorem OAI.Balanced.ProjectiveNormalization.image_filter_incident line 268
  26. theorem OAI.Balanced.ProjectiveNormalization.card_filter_incident line 278
  27. theorem OAI.Balanced.ProjectiveNormalization.card_skew_image line 284
  28. theorem OAI.Balanced.ProjectiveNormalization.card_tangents_image line 292
  29. theorem OAI.Balanced.ProjectiveNormalization.exists_tangent_normalization line 305
  30. theorem OAI.Balanced.ProjectiveNormalization.eq_affinePart_disjSum line 321
  31. theorem OAI.Balanced.ProjectiveNormalization.card_affinePart_add_one line 333
  32. theorem OAI.Balanced.ProjectiveNormalization.card_skew_codes line 339
  33. theorem OAI.Balanced.ProjectiveNormalization.exists_normalized_affine_set line 363
  34. theorem OAI.Balanced.ProjectiveNormalization.card_normalized_vertical_section line 379
  35. theorem OAI.Balanced.ProjectiveNormalization.card_normalized_infinity_section line 391
  36. theorem OAI.Balanced.ProjectiveNormalization.card_normalized_tangents line 400
  37. theorem OAI.Balanced.ProjectiveNormalization.exists_normalized_affine_set_with_tangents line 432