OAI/Geometry/HyperbolicGroups/InvolutionPairs.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.PictureSwitch.involution_swap_sq line 14
2. lemma OAI.HyperbolicObstruction.PictureSwitch.involution_swap_support line 26
3. lemma OAI.HyperbolicObstruction.PictureSwitch.involution_swap_card line 38
4. theorem OAI.HyperbolicObstruction.PictureSwitch.involution_pairs line 54

   Source documentation

   Every finite involution is a product of its actual paired points, with exactly half the support cardinal many transpositions.

   theorem involution_pairs (p : Perm D) (hp : p * p = 1) :
       ∃ l : List (D × D),
         (l.map (fun ab => swap ab.1 ab.2)).prod = p ∧
         2 * l.length = p.support.card ∧
         ∀ ab ∈ l, ab.1 ≠ ab.2 ∧ p ab.1 = ab.2 := by
   …