OAI/Combinatorics/EuclideanRamsey/NineGeometry.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Rational parametrization of the unit circle and its coordinate field.

  1. def OAI.EuclideanRamsey.NineGeometry.circlePoint line 12
  2. def OAI.EuclideanRamsey.NineGeometry.circleConfig line 15
  3. theorem OAI.EuclideanRamsey.NineGeometry.circlePoint_zero line 17
  4. theorem OAI.EuclideanRamsey.NineGeometry.circlePoint_one line 21
  5. theorem OAI.EuclideanRamsey.NineGeometry.circlePoint_recover line 25
  6. theorem OAI.EuclideanRamsey.NineGeometry.circlePoint_on_circle line 30
  7. theorem OAI.EuclideanRamsey.NineGeometry.circlePoint_injective line 33
  8. theorem OAI.EuclideanRamsey.NineGeometry.circleConfig_on_circle line 38
  9. theorem OAI.EuclideanRamsey.NineGeometry.circleConfig_injective line 41
  10. def OAI.EuclideanRamsey.NineGeometry.firstFive line 46

    Source documentation

    Restriction to the first five points.

    def firstFive (i : Fin 5) : Fin 9 := ⟨i.val, by omega⟩
  11. theorem OAI.EuclideanRamsey.NineGeometry.firstFive_injective line 48
  12. theorem OAI.EuclideanRamsey.NineGeometry.circleConfig_affineSpan line 53
  13. theorem OAI.EuclideanRamsey.NineGeometry.circleConfig_coordinateField line 67

    Source documentation

    The coordinate field is generated by the circle parameters.

    theorem circleConfig_coordinateField (t : Fin 9 → ℝ) :
    coordinateField (circleConfig t) = IntermediateField.adjoin ℚ (Set.range t) := by
…

    Mentions: OAI.EuclideanRamsey.coordinateField, OAI.EuclideanRamsey.NineGeometry.circleConfig