OAI/RingTheory/DirectFiniteness/CandidateModel.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.KaplanskyCounterexample.FiniteGeometry.(instance at line 13) line 13
  2. instance OAI.KaplanskyCounterexample.FiniteGeometry.(instance at line 21) line 21
  3. lemma OAI.KaplanskyCounterexample.FiniteGeometry.PolygonStep.eq_of_label_vector_eq line 28
  4. lemma OAI.KaplanskyCounterexample.FiniteGeometry.PolygonStep.vector_mem_label line 55
  5. structure OAI.KaplanskyCounterexample.FiniteGeometry.Candidate line 62
  6. lemma OAI.KaplanskyCounterexample.FiniteGeometry.Candidate.ext line 74
  7. instance OAI.KaplanskyCounterexample.FiniteGeometry.Candidate.(instance at line 77) line 77
  8. lemma OAI.KaplanskyCounterexample.FiniteGeometry.Candidate.closed line 82
  9. def OAI.KaplanskyCounterexample.FiniteGeometry.Candidate.labels line 85
  10. def OAI.KaplanskyCounterexample.FiniteGeometry.Candidate.positions line 87
  11. lemma OAI.KaplanskyCounterexample.FiniteGeometry.Candidate.count_eq_two line 89
  12. lemma OAI.KaplanskyCounterexample.FiniteGeometry.Candidate.labels_card_bounds line 93
  13. lemma OAI.KaplanskyCounterexample.FiniteGeometry.Candidate.positions_card line 99
  14. lemma OAI.KaplanskyCounterexample.FiniteGeometry.Candidate.points_eq line 103

    Source documentation

    Coordinate recovery on a cyclic sequence, used for the rooted event counts.

    lemma points_eq (c d : Candidate F T k) (hs : c.step = d.step) (i : Fin k)
    (hi : c.point i = d.point i) : c.point = d.point := by
…

    Mentions: OAI.KaplanskyCounterexample.FiniteGeometry.Candidate

  15. lemma OAI.KaplanskyCounterexample.FiniteGeometry.two_position_recovery line 132

    Source documentation

    In a closed vector sequence, deleting two positions in disjoint direction spaces leaves at most one completion. This supplies all polygon count uniqueness, including the unpaired sides of a pentagon.

    lemma two_position_recovery {I : Type u_5} [Fintype I] [DecidableEq I]
    (U W : Submodule Q A) (hUW : Disjoint U W) (a b : I) (hab : a ≠ b)
    (v v' : I → A) (ha : v a ∈ U) (ha' : v' a ∈ U)
    (hb : v b ∈ W) (hb' : v' b ∈ W)
    (hz : ∑ i, v i = 0) (hz' : ∑ i, v' i = 0)
    (he : ∀ i, i ≠ a → i ≠ b → v i = v' i) : v = v' := by
…