OAI/RingTheory/DirectFiniteness/CyclicLabels.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KaplanskyCounterexample.FiniteGeometry.cyclic_label_count_le_two line 13

   Source documentation

   In a cyclic sequence of at most five positions with unequal neighboring labels, no label can occur thrice. This includes the wrap-around adjacency.

   lemma cyclic_label_count_le_two {k : ℕ} {L : Type u_1} [DecidableEq L] (lab : Fin k → L)
       (hk : k ≤ 5) (hadj : ∀ i, lab i ≠ lab (finRotate k i)) (l : L) :
       ((Finset.univ : Finset (Fin k)).filter (fun i => lab i = l)).card ≤ 2 := by
   …

2. lemma OAI.KaplanskyCounterexample.FiniteGeometry.count_ne_one_of_sum_eq_zero line 30

   Source documentation

   A nonzero vector cannot be the sole contribution to a zero sum.

   lemma count_ne_one_of_sum_eq_zero {I : Type u_2} {L : Type u_3} {M : Type u_4} [Fintype I] [DecidableEq L]
       [AddCommGroup M] (lab : I → L) (v : I → M) (l : L)
       (hn : ∀ i, lab i = l → v i ≠ 0)
       (hz : ∑ i ∈ (Finset.univ : Finset I).filter (fun i => lab i = l), v i = 0) :
       ((Finset.univ : Finset I).filter (fun i => lab i = l)).card ≠ 1 := by
   …

3. lemma OAI.KaplanskyCounterexample.FiniteGeometry.cyclic_label_count_eq_two line 42
4. lemma OAI.KaplanskyCounterexample.FiniteGeometry.sum_label_counts line 57

   Source documentation

   Occurrence-count form of the pigeonhole bound, retaining the exact support.

   lemma sum_label_counts {I : Type u_7} {L : Type u_8} [Fintype I] [DecidableEq L] (lab : I → L) :
       ∑ l ∈ Finset.univ.image lab,
         ((Finset.univ : Finset I).filter (fun i => lab i = l)).card = Fintype.card I := by
   …