OAI/GroupTheory/Kervaire/Main.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KervaireRibbon.relator_ribbon_realized line 13
2. lemma OAI.KervaireRibbon.relator_normalClosure_coefficient_eq_one line 21
3. lemma OAI.Kervaire.normalClosure_coefficient_eq_one line 43

   Source documentation

   The finite relator indices range over positions, not over the possibly uncountable coefficient group. The original element and exponent are preserved.

   lemma normalClosure_coefficient_eq_one {A : Type*} [Group A] (w : WordGroup A)
       (hw : Unimodular w) (g : A) (hg : Coprod.inl g ∈ relatorClosure w) : g=1 := by
   …

   Mentions: OAI.Kervaire.WordGroup, OAI.Kervaire.Unimodular, OAI.Kervaire.relatorClosure

4. theorem OAI.Kervaire.coefficient_injective line 86

   Distinct definitions of this name: ComparatorChallenges/Kervaire.lean:31 (same statement text; different proof or body). Qualify references as OAI.Kervaire.coefficient_injective@path.

5. theorem OAI.Kervaire.quotient_nontrivial line 90